defpred S1[ 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: S1[ 0 ] by Lm1;
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; :: thesis: ( S1[B] implies S1[ succ B] )
assume Tarski-Class (X,B) is Subset of (Tarski-Class X) ; :: thesis: S1[ 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 S1[ 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
S1[C] ) holds
S1[B]
proof
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[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: S1[B]
deffunc H1( 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 = H1(C) ) ) from ORDINAL2:sch 2();
 Tarski-Class (X,B) = (union (rng L)) /\ (Tarski-Class X) by A6, A7, Lm1;
hence S1[B] by XBOOLE_1:17; :: thesis: verum
end;
for A being Ordinal holds S1[A] from ORDINAL2:sch 1(A1, A2, A5);
 hence Tarski-Class (X,A) is Subset of (Tarski-Class X) ; :: thesis: verum