defpred S₁[ Ordinal] means Tarski-Class X,$1 is Subset of (Tarski-Class X);
A1: {X} c= Tarski-Class X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} or x in Tarski-Class X )
assume A2: x in {X} ; :: thesis: x in Tarski-Class X
A3: x = X by A2, TARSKI:def 1;
thus x in Tarski-Class X by A3, Th5; :: thesis: verum

end;

A4: S₁[ {} ] by A1, Lm1;
A5: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A6: Tarski-Class X,B is Subset of (Tarski-Class X) ; :: thesis: S₁[ succ B]
reconsider S = Tarski-Class X,B as Subset of (Tarski-Class X) by A6;
set Y = Tarski-Class X,(succ B);
A7: Tarski-Class X,(succ B) c= Tarski-Class X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Tarski-Class X,(succ B) or x in Tarski-Class X )
assume A8: x in Tarski-Class X,(succ B) ; :: thesis: x in Tarski-Class X
A9: x in ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in S & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in S } ) \/ ((bool S) /\ (Tarski-Class X)) by A8, Lm1;
A10: ( x in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in S & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in S } or x in (bool S) /\ (Tarski-Class X) ) by A9, XBOOLE_0:def 3;

A11: now

assume A12: x in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in S & u c= v ) } ; :: thesis: x in Tarski-Class X
A13: ex u being Element of Tarski-Class X st
( x = u & ex v being Element of Tarski-Class X st
( v in S & u c= v ) ) by A12;
thus x in Tarski-Class X by A13; :: thesis: verum

end;

A14: now

assume A15: x in { (bool v) where v is Element of Tarski-Class X : v in S } ; :: thesis: x in Tarski-Class X
A16: ex v being Element of Tarski-Class X st
( x = bool v & v in S ) by A15;
thus x in Tarski-Class X by A16, Th7; :: thesis: verum

end;

thus x in Tarski-Class X by A10, A11, A14, XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

end;

thus S₁[ succ B] by A7; :: thesis: verum

end;

A17: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume that
A18: ( B <> {} & B is limit_ordinal ) and
for C being Ordinal st C in B holds
Tarski-Class X,C is Subset of (Tarski-Class X) ; :: thesis: S₁[B]
deffunc H₁( Ordinal) -> set = Tarski-Class X,$1;
consider L being T-Sequence such that
A19: ( dom L = B & ( for C being Ordinal st C in B holds
L . C = H₁(C) ) ) from ORDINAL2:sch 2();
A20: Tarski-Class X,B = (union (rng L)) /\ (Tarski-Class X) by A18, A19, Lm1;
thus S₁[B] by A20, XBOOLE_1:17; :: thesis: verum

end;

A21: for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A4, A5, A17);
thus Tarski-Class X,A is Subset of (Tarski-Class X) by A21; :: thesis: verum