let X be set ; :: thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
Tarski-Class X,A = { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) }
let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies Tarski-Class X,A = { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } )
assume A1: ( A <> {} & A is limit_ordinal ) ; :: thesis: Tarski-Class X,A = { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) }
deffunc H₁( Ordinal) -> Subset of (Tarski-Class X) = Tarski-Class X,$1;
consider L being T-Sequence such that
A2: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(B) ) ) from ORDINAL2:sch 2();
A3: Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X) by A1, A2, Lm1;
thus Tarski-Class X,A c= { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } :: according to XBOOLE_0:def 10 :: thesis: { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } c= Tarski-Class X,A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Tarski-Class X,A or x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } )
assume x in Tarski-Class X,A ; :: thesis: x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) }
then x in union (rng L) by A3, XBOOLE_0:def 4;
then consider Y being set such that
A4: ( x in Y & Y in rng L ) by TARSKI:def 4;
consider y being set such that
A5: ( y in dom L & Y = L . y ) by A4, FUNCT_1:def 5;
reconsider y = y as Ordinal by A5;
Y = Tarski-Class X,y by A2, A5;
hence x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } by A2, A4, A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } or x in Tarski-Class X,A )
assume x in { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) } ; :: thesis: x in Tarski-Class X,A
then consider u being Element of Tarski-Class X such that
A6: ( x = u & ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) ) ;
consider B being Ordinal such that
A7: ( B in A & u in Tarski-Class X,B ) by A6;
L . B = Tarski-Class X,B by A2, A7;
then Tarski-Class X,B in rng L by A2, A7, FUNCT_1:def 5;
then ( u in union (rng L) & u in Tarski-Class X ) by A7, TARSKI:def 4;
hence x in Tarski-Class X,A by A3, A6, XBOOLE_0:def 4; :: thesis: verum