let H be ZF-formula; :: thesis: Free H is finite
defpred S₁[ ZF-formula] means Free $1 is finite ;
A1: for p, q being ZF-formula st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be ZF-formula; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
Free (p '&' q) = (Free p) \/ (Free q) by Th66;
hence ( S₁[p] & S₁[q] implies S₁[p '&' q] ) ; :: thesis: verum

end;

A2: for p being ZF-formula
for x being Variable st S₁[p] holds
S₁[ All x,p]

proof

let p be ZF-formula; :: thesis: for x being Variable st S₁[p] holds
S₁[ All x,p]
let x be Variable; :: thesis: ( S₁[p] implies S₁[ All x,p] )
Free (All x,p) = (Free p) \ {x} by Th67;
hence ( S₁[p] implies S₁[ All x,p] ) ; :: thesis: verum

end;

A3: for x, y being Variable holds
( S₁[x '=' y] & S₁[x 'in' y] )

proof

let x, y be Variable; :: thesis: ( S₁[x '=' y] & S₁[x 'in' y] )
Free (x '=' y) = {x,y} by Th63;
hence ( S₁[x '=' y] & S₁[x 'in' y] ) by Th64; :: thesis: verum

end;

A4: for p being ZF-formula st S₁[p] holds
S₁[ 'not' p] by Th65;
for p being ZF-formula holds S₁[p] from ZF_LANG1:sch 1(A3, A4, A1, A2);
hence Free H is finite ; :: thesis: verum