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 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 object ; :: 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 and
A5: Y in rng L by TARSKI:def 4;
consider y being object such that
A6: y in dom L and
A7: Y = L . y by A5, FUNCT_1:def 3;
reconsider y = y as Ordinal by A6;
Y = Tarski-Class (X,y) by A2, A6, A7;
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, A6; :: thesis: verum

end;

let x be object ; :: 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
A8: x = u and
A9: ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) ;
consider B being Ordinal such that
A10: B in A and
A11: u in Tarski-Class (X,B) by A9;
L . B = Tarski-Class (X,B) by A2, A10;
then Tarski-Class (X,B) in rng L by A2, A10, FUNCT_1:def 3;
then u in union (rng L) by A11, TARSKI:def 4;
hence x in Tarski-Class (X,A) by A3, A8, XBOOLE_0:def 4; :: thesis: verum