defpred S1[ ZF-formula] means Free H is finite ;
A1: for p, q being ZF-formula st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be ZF-formula; :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
Free (p '&' q) = (Free p) \/ (Free q) by Th61;
hence ( S1[p] & S1[q] implies S1[p '&' q] ) ; :: thesis: verum
end;
A2: for p being ZF-formula
for x being Variable st S1[p] holds
S1[ All (x,p)]
proof
let p be ZF-formula; :: thesis: for x being Variable st S1[p] holds
S1[ All (x,p)]
let x be Variable; :: thesis: ( S1[p] implies S1[ All (x,p)] )
Free (All (x,p)) = (Free p) \ {x} by Th62;
hence ( S1[p] implies S1[ All (x,p)] ) ; :: thesis: verum
end;
A3: for x, y being Variable holds
( S1[x '=' y] & S1[x 'in' y] )
proof
let x, y be Variable; :: thesis: ( S1[x '=' y] & S1[x 'in' y] )
Free (x '=' y) = {x,y} by Th58;
hence ( S1[x '=' y] & S1[x 'in' y] ) by Th59; :: thesis: verum
end;
A4: for p being ZF-formula st S1[p] holds
S1[ 'not' p] by Th60;
for p being ZF-formula holds S1[p] from ZF_LANG1:sch 1(A3, A4, A1, A2);
 hence Free H is finite ; :: thesis: verum