let x, y, z be Variable; :: thesis: for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
let H be ZF-formula; :: thesis: for E being non empty set
for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
let E be non empty set ; :: thesis: for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
let f be Function of VAR,E; :: thesis: ( {x,y,z} misses Free H & E,f |= H implies E,f |= All (x,y,z,H) )
assume that
A1: {x,y,z} misses Free H and
A2: E,f |= H ; :: thesis: E,f |= All (x,y,z,H)
A3: bound_in (All (y,(All (z,H)))) = y by Lm2;

now :: thesis: for a being object st a in {y,z} holds
not a in Free H

let a be object ; :: thesis: ( a in {y,z} implies not a in Free H )
assume a in {y,z} ; :: thesis: not a in Free H
then ( a = y or a = z ) by TARSKI:def 2;
then a in {x,y,z} by ENUMSET1:def 1;
hence not a in Free H by A1, XBOOLE_0:3; :: thesis: verum

end;

then {y,z} misses Free H by XBOOLE_0:3;
then A4: E,f |= All (y,z,H) by A2, Th11;
A5: ( All (z,H) is universal & the_scope_of (All (z,H)) = H ) by Lm2;
x in {x,y,z} by ENUMSET1:def 1;
then not x in Free H by A1, XBOOLE_0:3;
then not x in (Free H) \ {z} by XBOOLE_0:def 5;
then A6: not x in ((Free H) \ {z}) \ {y} by XBOOLE_0:def 5;
A7: bound_in (All (z,H)) = z by Lm2;
( All (y,(All (z,H))) is universal & the_scope_of (All (y,(All (z,H)))) = All (z,H) ) by Lm2;
then Free (All (y,z,H)) = (Free (All (z,H))) \ {y} by A3, ZF_MODEL:1
.= ((Free H) \ {z}) \ {y} by A5, A7, ZF_MODEL:1 ;
hence E,f |= All (x,y,z,H) by A4, A6, Th10; :: thesis: verum