let V be Universe; :: thesis: for X being Subclass of V st X is closed_wrt_A1-A7 holds
omega c= X
let X be Subclass of V; :: thesis: ( X is closed_wrt_A1-A7 implies omega c= X )
assume A1: X is closed_wrt_A1-A7 ; :: thesis: omega c= X
assume not omega c= X ; :: thesis: contradiction
then consider o being set such that
A2: ( o in omega & not o in X ) by TARSKI:def 3;
reconsider K = o as Ordinal by A2;
defpred S₁[ Ordinal] means ( $1 in omega & not $1 in X );
( K in omega & not K in X ) by A2;
then A3: ex K being Ordinal st S₁[K] ;
consider L being Ordinal such that
A4: ( S₁[L] & ( for M being Ordinal st S₁[M] holds
L c= M ) ) from ORDINAL1:sch 1(A3);
L <> {} by A1, A4, Th3;
then A5: {} in L by ORDINAL3:10;
A6: L c= omega by A4;
not omega c= L by A4;
then not L is limit_ordinal by A5, ORDINAL1:def 12;
then consider M being Ordinal such that
A9: succ M = L by ORDINAL1:42;
A10: M in L by A9, ORDINAL1:10;

A11: now

assume not M in X ; :: thesis: contradiction
then A12: L c= M by A4, A6, A10;
M c= L by A10, ORDINAL1:def 2;
then M = L by A12, XBOOLE_0:def 10;
hence contradiction by A9, ORDINAL1:14; :: thesis: verum

end;

then {M} in X by A1, Th2;
then M \/ {M} in X by A1, A11, Th4;
hence contradiction by A4, A9, ORDINAL1:def 1; :: thesis: verum