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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} or x in Tarski-Class X )
assume x in {X} ; :: thesis: x in Tarski-Class X
then x = X by TARSKI:def 1;
hence x in Tarski-Class X by Th2; :: thesis: verum

end;

then A1: S₁[ 0 ] by Lm1;
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 Tarski-Class (X,B) is Subset of (Tarski-Class X) ; :: thesis: S₁[ succ B]
then reconsider S = Tarski-Class (X,B) as Subset of (Tarski-Class X) ;
set Y = Tarski-Class (X,(succ B));
Tarski-Class (X,(succ B)) c= Tarski-Class X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Tarski-Class (X,(succ B)) or x in Tarski-Class X )
assume x in Tarski-Class (X,(succ B)) ; :: thesis: x in Tarski-Class X
then 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 Lm1;
then A3: ( 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 XBOOLE_0:def 3;

A4: now :: thesis: ( 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 ) } implies x in Tarski-Class X )

assume 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
then 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 ) ) ;
hence x in Tarski-Class X ; :: thesis: verum

end;

now :: thesis: ( x in { (bool v) where v is Element of Tarski-Class X : v in S } implies x in Tarski-Class X )

assume x in { (bool v) where v is Element of Tarski-Class X : v in S } ; :: thesis: x in Tarski-Class X
then ex v being Element of Tarski-Class X st
( x = bool v & v in S ) ;
hence x in Tarski-Class X by Th4; :: thesis: verum

end;

hence x in Tarski-Class X by A3, A4, XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum

end;

hence S₁[ succ B] ; :: thesis: verum

end;

A5: for B being Ordinal st B <> 0 & 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 <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume that
A6: ( B <> 0 & 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 Sequence such that
A7: ( dom L = B & ( for C being Ordinal st C in B holds
L . C = H₁(C) ) ) from ORDINAL2:sch 2();
Tarski-Class (X,B) = (union (rng L)) /\ (Tarski-Class X) by A6, A7, Lm1;
hence S₁[B] by XBOOLE_1:17; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A1, A2, A5);
hence Tarski-Class (X,A) is Subset of (Tarski-Class X) ; :: thesis: verum