1. {0}εx  DxH1 =  2. K: {0}εxK =  & KDxH1 =  D3. 3. K: {0}(x) =  & {0} x K & K = H1 & K(x) ∈ D D3.εu, β 4. KA: {0}[x/A] = K & K = H1 & K(x) ∈ D D2.0, G u H 5. A: {0}[x/A] = H1 & H1(x) ∈ D elim. K 6. A: {0}[x/A] = H1 & A{} ∈ D D2.G...