let H be ZF-formula; :: thesis: for x, y being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
let x, y be Variable; :: thesis: ( not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 implies ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) )
A1: x. 0 <> x. 3 by ZF_LANG1:76;
assume that
A2: not y in variables_in H and
A3: x <> x. 0 and
A4: y <> x. 0 and
A5: y <> x. 4 ; :: thesis: ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
set G = (H / ((x. 0),y)) / ((x. 4),(x. 0));
A6: Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) = (Free (((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:66
.= ((Free ((x. 3) 'in' x)) \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:61
.= ({(x. 3),x} \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:59
.= ({(x. 3),x} \ {(x. 3)}) \/ ((Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)}) by XBOOLE_1:42 ;
A7: x. 0 <> x. 4 by ZF_LANG1:76;

A8: now :: thesis: ( x. 4 in Free H implies x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )

assume A9: x. 4 in Free H ; :: thesis: x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))))
A10: x. 4 in Free (H / ((x. 0),y))

proof

now :: thesis: x. 4 in Free (H / ((x. 0),y))

per cases ( x. 0 in Free H or not x. 0 in Free H ) ;

suppose A11: x. 0 in Free H ; :: thesis: x. 4 in Free (H / ((x. 0),y))

not x. 4 in {(x. 0)} by A7, TARSKI:def 1;
then A12: x. 4 in (Free H) \ {(x. 0)} by A9, XBOOLE_0:def 5;
Free (H / ((x. 0),y)) = ((Free H) \ {(x. 0)}) \/ {y} by A2, A11, ZFMODEL2:2;
hence x. 4 in Free (H / ((x. 0),y)) by A12, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x. 0 in Free H ; :: thesis: x. 4 in Free (H / ((x. 0),y))

hence x. 4 in Free (H / ((x. 0),y)) by A2, A9, ZFMODEL2:2; :: thesis: verum

end;

end;

end;

hence x. 4 in Free (H / ((x. 0),y)) ; :: thesis: verum

end;

A13: x. 0 in {(x. 0)} by TARSKI:def 1;
not x. 0 in variables_in (H / ((x. 0),y)) by A4, ZF_LANG1:184;
then Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) = ((Free (H / ((x. 0),y))) \ {(x. 4)}) \/ {(x. 0)} by A10, ZFMODEL2:2;
then A14: x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) by A13, XBOOLE_0:def 3;
not x. 0 in {(x. 3)} by A1, TARSKI:def 1;
then x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} by A14, XBOOLE_0:def 5;
hence x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

now :: thesis: ( x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) implies x. 4 in Free H )

assume x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ; :: thesis: x. 4 in Free H
then ( x. 0 in {(x. 3),x} \ {(x. 3)} or x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} ) by A6, XBOOLE_0:def 3;
then A15: ( x. 0 in {(x. 3),x} or x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) ) by XBOOLE_0:def 5;
A16: not x. 0 in variables_in (H / ((x. 0),y)) by A4, ZF_LANG1:184;

A17: now :: thesis: x. 4 in Free (H / ((x. 0),y))

assume not x. 4 in Free (H / ((x. 0),y)) ; :: thesis: contradiction
then A18: x. 0 in Free (H / ((x. 0),y)) by A3, A1, A15, A16, TARSKI:def 2, ZFMODEL2:2;
Free (H / ((x. 0),y)) c= variables_in (H / ((x. 0),y)) by ZF_LANG1:151;
hence contradiction by A4, A18, ZF_LANG1:184; :: thesis: verum

end;

Free (H / ((x. 0),y)) c= ((Free H) \ {(x. 0)}) \/ {y} by ZFMODEL2:1;
then ( x. 4 in (Free H) \ {(x. 0)} or x. 4 in {y} ) by A17, XBOOLE_0:def 3;
hence x. 4 in Free H by A5, TARSKI:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

hence ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) by A8; :: thesis: verum