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
A6: x in Y and
A7: Y in rng L by TARSKI:def 4;
consider y being set such that
A8: y in dom L and
A9: Y = L . y by A7, FUNCT_1:def 5;
reconsider y = y as Ordinal by A8;
Y = Tarski-Class X,y by A2, A8, A9;
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, A6, A8; :: 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
A12: x = u and
A13: ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) ;
consider B being Ordinal such that
A14: B in A and
A15: u in Tarski-Class X,B by A13;
L . B = Tarski-Class X,B by A2, A14;
then Tarski-Class X,B in rng L by A2, A14, FUNCT_1:def 5;
then u in union (rng L) by A15, TARSKI:def 4;
hence x in Tarski-Class X,A by A3, A12, XBOOLE_0:def 4; :: thesis: verum