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 A1: ( X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds
o in X ) ) ; :: thesis: B in X
then A2: S₁[ {} ] by Th3;
A3: B is finite by A1;
A4: 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 A5: ( o in B & C c= B & C in X ) ; :: thesis: S₁[C \/ {o}]
then o in X by A1;
then {o} in X by A1, Th2;
hence S₁[C \/ {o}] by A1, A5, Th4; :: thesis: verum

end;

thus S₁[B] from FINSET_1:sch 2(A3, A2, A4); :: thesis: verum