let V be Universe; :: thesis:
let X be Subclass of V; :: thesis:
let B be set ; :: thesis:
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:
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}]

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

end;