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 object such that
A2: o in omega and
A3: not o in X ;
defpred S1[ Ordinal] means ( $1 in omega & not $1 in X );
A4: ex K being Ordinal st S1[K] by A2, A3;
consider L being Ordinal such that
A5: ( S1[L] & ( for M being Ordinal st S1[M] holds
L c= M ) ) from ORDINAL1:sch 1(A4);
 L <> {} by A1, A5, Th3;
then A6: {} in L by ORDINAL3:8;
not omega c= L by A5;
then not L is limit_ordinal by A6, ORDINAL1:def 11;
then consider M being Ordinal such that
A7: succ M = L by ORDINAL1:29;
A8: M in L by A7, ORDINAL1:6;
A9: L c= omega by A5;
A10: now :: thesis: M in X
assume not M in X ; :: thesis: contradiction
then A11: L c= M by A5, A9, A8;
M c= L by A8, ORDINAL1:def 2;
then M = L by A11;
hence contradiction by A7, ORDINAL1:9; :: thesis: verum
end;
then {M} in X by A1, Th2;
then M \/ {M} in X by A1, A10, Th4;
hence contradiction by A5, A7; :: thesis: verum