let V be Universe; :: thesis: for X being Subclass of V
for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds
o in X ) holds
B in X
let X be Subclass of V; :: thesis: for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds
o in X ) holds
B in X
let B be set ; :: thesis: ( X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds
o in X ) implies B in X )
defpred S₁[ set ] means $1 in X;
assume that
A1: X is closed_wrt_A1-A7 and
A2: B is finite and
A3: for o being set st o in B holds
o in X ; :: thesis: B in X
A4: B is finite by A2;
A5: for o, C being set st o in B & C c= B & S₁[C] holds
S₁[C \/ {o}]

proof

let o, C be set ; :: thesis: ( o in B & C c= B & S₁[C] implies S₁[C \/ {o}] )
assume that
A6: o in B and
C c= B and
A7: C in X ; :: thesis: S₁[C \/ {o}]
o in X by A3, A6;
then {o} in X by A1, Th2;
hence S₁[C \/ {o}] by A1, A7, Th4; :: thesis: verum

end;

A8: S₁[ {} ] by A1, Th3;
thus S₁[B] from FINSET_1:sch 2(A4, A8, A5); :: thesis: verum