let H be ZF-formula; :: thesis: ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )

defpred S2[ Nat] means for H being ZF-formula st card (Free H) = \$1 holds
ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) );
A1: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A2: S2[i] ; :: thesis: S2[i + 1]
let H be ZF-formula; :: thesis: ( card (Free H) = i + 1 implies ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) )

set e = the Element of Free H;
assume A3: card (Free H) = i + 1 ; :: thesis: ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )

then A4: Free H <> {} ;
then reconsider x = the Element of Free H as Variable by TARSKI:def 3;
A5: {x} c= Free H by ;
A6: Free (All (x,H)) = (Free H) \ {x} by ZF_LANG1:62;
x in {x} by ZFMISC_1:31;
then A7: not x in Free (All (x,H)) by ;
(Free (All (x,H))) \/ {x} = (Free H) \/ {x} by ;
then (Free (All (x,H))) \/ {x} = Free H by ;
then (card (Free (All (x,H)))) + 1 = card (Free H) by ;
then consider S being ZF-formula such that
A8: Free S = {} and
A9: for M being non empty set holds
( M |= S iff M |= All (x,H) ) by ;
take S ; :: thesis: ( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )

thus Free S = {} by A8; :: thesis: for M being non empty set holds
( M |= S iff M |= H )

let M be non empty set ; :: thesis: ( M |= S iff M |= H )
( M |= H iff M |= All (x,H) ) by ZF_MODEL:23;
hence ( M |= S iff M |= H ) by A9; :: thesis: verum
end;
A10: card (Free H) = card (Free H) ;
A11: S2[ 0 ]
proof
let H be ZF-formula; :: thesis: ( card (Free H) = 0 implies ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) )

assume A12: card (Free H) = 0 ; :: thesis: ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )

take H ; :: thesis: ( Free H = {} & ( for M being non empty set holds
( M |= H iff M |= H ) ) )

thus ( Free H = {} & ( for M being non empty set holds
( M |= H iff M |= H ) ) ) by A12; :: thesis: verum
end;
for i being Nat holds S2[i] from NAT_1:sch 2(A11, A1);
hence ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) by A10; :: thesis: verum