defpred S2[ Ordinal] means UNIVERSE A is Universe;
A1: for B being Ordinal st S2[B] holds
S2[ succ B]
proof
let B be Ordinal; :: thesis: ( S2[B] implies S2[ succ B] )
assume S2[B] ; :: thesis: S2[ succ B]
then reconsider UU = UNIVERSE B as Universe ;
UNIVERSE (succ B) = Tarski-Class UU by Lm6;
hence S2[ succ B] ; :: thesis: verum
end;
A2: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S2[B] ) holds
S2[A]
proof
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S2[B] ) implies S2[A] )
assume that
A3: A <> 0 and
A4: A is limit_ordinal and
for B being Ordinal st B in A holds
S2[B] ; :: thesis: S2[A]
consider L being Sequence such that
A5: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) ) from ORDINAL2:sch 2();
 UNIVERSE A = Universe_closure (Union L) by A3, A4, A5, Lm6
.= Universe_closure (union (rng L)) by CARD_3:def 4 ;
hence S2[A] ; :: thesis: verum
end;
A6: S2[ 0 ] by Lm6;
for A being Ordinal holds S2[A] from ORDINAL2:sch 1(A6, A1, A2);
 hence ( UNIVERSE A is universal & not UNIVERSE A is empty ) ; :: thesis: verum