let H be ZF-formula; :: thesis:
defpred S₂[ Element of 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: S₂[ 0 ]

let H be ZF-formula; :: thesis:
assume A2: card (Free H) = 0 ; :: thesis:
take H ; :: thesis:
thus ( Free H = {} & ( for M being non empty set holds
( M |= H iff M |= H ) ) ) by A2; :: thesis:

end;

A3: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

let i be Element of NAT ; :: thesis:
assume A4: S₂[i] ; :: thesis:
let H be ZF-formula; :: thesis:
assume A5: card (Free H) = i + 1 ; :: thesis:
then A6: Free H <> {} by CARD_1:47, NAT_1:5;
consider e being Element of Free H;
reconsider x = e as Variable by A6, TARSKI:def 3;
A7: Free (All x,H) = (Free H) \ {x} by ZF_LANG1:67;
then ( (Free (All x,H)) \/ {x} = (Free H) \/ {x} & {x} c= Free H & x in {x} ) by A6, XBOOLE_1:39, ZFMISC_1:37;
then ( Free (All x,H) is finite & (Free (All x,H)) \/ {x} = Free H & not x in Free (All x,H) ) by A7, XBOOLE_0:def 5, XBOOLE_1:12;
then (card (Free (All x,H))) + 1 = card (Free H) by CARD_2:54;
then card (Free (All x,H)) = i by A5, XCMPLX_1:2;
then consider S being ZF-formula such that
A8: ( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= All x,H ) ) ) by A4;
take S ; :: thesis:
thus Free S = {} by A8; :: thesis:
let M be non empty set ; :: thesis:
( M |= H iff M |= All x,H ) by ZF_MODEL:25;
hence ( M |= S iff M |= H ) by A8; :: thesis:

end;

A9: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A1, A3);
card (Free H) = card (Free H) ;
hence ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) by A9; :: thesis: