let x, y be Variable; :: thesis: for H being ZF-formula holds Free (H / x,y) c= ((Free H) \ {x}) \/ {y}
let H be ZF-formula; :: thesis: Free (H / x,y) c= ((Free H) \ {x}) \/ {y}
defpred S₁[ ZF-formula] means Free ($1 / x,y) c= ((Free $1) \ {x}) \/ {y};
A1: for x1, x2 being Variable holds
( S₁[x1 '=' x2] & S₁[x1 'in' x2] )

proof

let x1, x2 be Variable; :: thesis: ( S₁[x1 '=' x2] & S₁[x1 'in' x2] )
( ( x1 = x or x1 <> x ) & ( x2 = x or x2 <> x ) ) ;
then consider y1, y2 being Variable such that
A2: ( ( x1 <> x & x2 <> x & y1 = x1 & y2 = x2 ) or ( x1 = x & x2 <> x & y1 = y & y2 = x2 ) or ( x1 <> x & x2 = x & y1 = x1 & y2 = y ) or ( x1 = x & x2 = x & y1 = y & y2 = y ) ) ;
( (x1 '=' x2) / x,y = y1 '=' y2 & (x1 'in' x2) / x,y = y1 'in' y2 ) by A2, ZF_LANG1:166, ZF_LANG1:168;
then A3: ( Free ((x1 '=' x2) / x,y) = {y1,y2} & Free (x1 '=' x2) = {x1,x2} & Free ((x1 'in' x2) / x,y) = {y1,y2} & Free (x1 'in' x2) = {x1,x2} ) by ZF_LANG1:63, ZF_LANG1:64;
{y1,y2} c= ({x1,x2} \ {x}) \/ {y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {y1,y2} or a in ({x1,x2} \ {x}) \/ {y} )
assume a in {y1,y2} ; :: thesis: a in ({x1,x2} \ {x}) \/ {y}
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A2, TARSKI:def 2;
then ( ( a in {x1,x2} & not a in {x} ) or a in {y} ) by TARSKI:def 1, TARSKI:def 2;
then ( a in {x1,x2} \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in ({x1,x2} \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

hence ( S₁[x1 '=' x2] & S₁[x1 'in' x2] ) by A3; :: thesis: verum

end;

A4: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H]

proof

let H be ZF-formula; :: thesis: ( S₁[H] implies S₁[ 'not' H] )
( Free ('not' (H / x,y)) = Free (H / x,y) & Free ('not' H) = Free H & ('not' H) / x,y = 'not' (H / x,y) ) by ZF_LANG1:65, ZF_LANG1:170;
hence ( S₁[H] implies S₁[ 'not' H] ) ; :: thesis: verum

end;

A5: for H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

proof

let H1, H2 be ZF-formula; :: thesis: ( S₁[H1] & S₁[H2] implies S₁[H1 '&' H2] )
assume ( S₁[H1] & S₁[H2] ) ; :: thesis: S₁[H1 '&' H2]
then A6: ( Free ((H1 / x,y) '&' (H2 / x,y)) = (Free (H1 / x,y)) \/ (Free (H2 / x,y)) & Free (H1 '&' H2) = (Free H1) \/ (Free H2) & (H1 '&' H2) / x,y = (H1 / x,y) '&' (H2 / x,y) & (Free (H1 / x,y)) \/ (Free (H2 / x,y)) c= (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) ) by XBOOLE_1:13, ZF_LANG1:66, ZF_LANG1:172;
(((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) c= (((Free H1) \/ (Free H2)) \ {x}) \/ {y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) or a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y} )
assume a in (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) ; :: thesis: a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y}
then ( a in ((Free H1) \ {x}) \/ {y} or a in ((Free H2) \ {x}) \/ {y} ) by XBOOLE_0:def 3;
then ( a in (Free H1) \ {x} or a in (Free H2) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( ( a in Free H1 or a in Free H2 ) & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( ( a in (Free H1) \/ (Free H2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def 3;
then ( a in ((Free H1) \/ (Free H2)) \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

hence S₁[H1 '&' H2] by A6, XBOOLE_1:1; :: thesis: verum

end;

A7: for H being ZF-formula
for z being Variable st S₁[H] holds
S₁[ All z,H]

proof

let H be ZF-formula; :: thesis: for z being Variable st S₁[H] holds
S₁[ All z,H]
let z be Variable; :: thesis: ( S₁[H] implies S₁[ All z,H] )
( z = x or z <> x ) ;
then consider s being Variable such that
A8: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
assume S₁[H] ; :: thesis: S₁[ All z,H]
then A9: ( Free (All s,(H / x,y)) = (Free (H / x,y)) \ {s} & Free (All z,H) = (Free H) \ {z} & (All z,H) / x,y = All s,(H / x,y) & (Free (H / x,y)) \ {s} c= (((Free H) \ {x}) \/ {y}) \ {s} ) by A8, XBOOLE_1:33, ZF_LANG1:67, ZF_LANG1:173, ZF_LANG1:174;
(((Free H) \ {x}) \/ {y}) \ {s} c= (((Free H) \ {z}) \ {x}) \/ {y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (((Free H) \ {x}) \/ {y}) \ {s} or a in (((Free H) \ {z}) \ {x}) \/ {y} )
assume A10: a in (((Free H) \ {x}) \/ {y}) \ {s} ; :: thesis: a in (((Free H) \ {z}) \ {x}) \/ {y}
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( a in Free H & not a in {z} & not a in {x} ) or a in {y} ) by A8, A10, XBOOLE_0:def 5;
then ( ( a in (Free H) \ {z} & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( a in ((Free H) \ {z}) \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in (((Free H) \ {z}) \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

hence S₁[ All z,H] by A9, XBOOLE_1:1; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A1, A4, A5, A7);
hence Free (H / x,y) c= ((Free H) \ {x}) \/ {y} ; :: thesis: verum