defpred S₁[ ZF-formula] means Free H 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 Th61;
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 Th62;
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 Th58;
hence ( S₁[x '=' y] & S₁[x 'in' y] ) by Th59; :: thesis: verum

end;

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