let A, B be Ordinal; :: thesis: ( A in B iff UNIVERSE A in UNIVERSE B )
defpred S₂[ Ordinal] means for A being Ordinal st A in $1 holds
UNIVERSE A in UNIVERSE $1;
A1: S₂[ {} ] ;
A2: for B being Ordinal st S₂[B] holds
S₂[ succ B]

proof

let B be Ordinal; :: thesis: ( S₂[B] implies S₂[ succ B] )
assume A3: S₂[B] ; :: thesis: S₂[ succ B]
let A be Ordinal; :: thesis: ( A in succ B implies UNIVERSE A in UNIVERSE (succ B) )
A4: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def 8;
assume A in succ B ; :: thesis: UNIVERSE A in UNIVERSE (succ B)
then ( UNIVERSE (succ B) = Tarski-Class (UNIVERSE B) & A c= B ) by Lm6, ORDINAL1:34;
then A5: ( UNIVERSE B in UNIVERSE (succ B) & ( A in B or A = B ) ) by A4, CLASSES1:5, ORDINAL1:21;
then ( UNIVERSE A in UNIVERSE B or UNIVERSE A = UNIVERSE B ) by A3;
hence UNIVERSE A in UNIVERSE (succ B) by A5, Th59; :: thesis: verum

end;

A6: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₂[B] ) holds
S₂[A]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for B being Ordinal st B in B holds
S₂[B] ) implies S₂[B] )
assume that
A7: ( B <> {} & B is limit_ordinal ) and
for C being Ordinal st C in B holds
for A being Ordinal st A in C holds
UNIVERSE A in UNIVERSE C ; :: thesis: S₂[B]
let A be Ordinal; :: thesis: ( A in B implies UNIVERSE A in UNIVERSE B )
assume A in B ; :: thesis: UNIVERSE A in UNIVERSE B
then A8: succ A in B by A7, ORDINAL1:41;
consider L being T-Sequence such that
A9: ( dom L = B & ( for C being Ordinal st C in B holds
L . C = H₅(C) ) ) from ORDINAL2:sch 2();
A10: UNIVERSE B = Universe_closure (Union L) by A7, A9, Lm6
.= Universe_closure (union (rng L)) by CARD_3:def 4 ;
L . (succ A) = UNIVERSE (succ A) by A8, A9;
then UNIVERSE (succ A) in rng L by A8, A9, FUNCT_1:def 5;
then ( UNIVERSE (succ A) c= union (rng L) & union (rng L) c= UNIVERSE B ) by A10, Def4, ZFMISC_1:92;
then ( UNIVERSE A in Tarski-Class (UNIVERSE A) & UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) & UNIVERSE (succ A) c= UNIVERSE B ) by Lm6, CLASSES1:5, XBOOLE_1:1;
hence UNIVERSE A in UNIVERSE B ; :: thesis: verum

end;

A11: for B being Ordinal holds S₂[B] from ORDINAL2:sch 1(A1, A2, A6);
hence ( A in B implies UNIVERSE A in UNIVERSE B ) ; :: thesis: ( UNIVERSE A in UNIVERSE B implies A in B )
assume A12: ( UNIVERSE A in UNIVERSE B & not A in B ) ; :: thesis: contradiction
( B c< A iff ( B c= A & B <> A ) ) by XBOOLE_0:def 8;
then ( B in A or B = A ) by A12, ORDINAL1:21, ORDINAL1:26;
hence contradiction by A11, A12; :: thesis: verum