let X, x be set ; :: thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
( x in Tarski-Class X,A iff ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) )
let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies ( x in Tarski-Class X,A iff ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) ) )
assume A1: ( A <> {} & A is limit_ordinal ) ; :: thesis: ( x in Tarski-Class X,A iff ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) )
A2: 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 ) } by A1, Th12;
thus ( x in Tarski-Class X,A implies ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) ) :: thesis: ( ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) implies x in Tarski-Class X,A )

proof

assume A3: x in Tarski-Class X,A ; :: thesis: ex B being Ordinal st
( B in A & x in Tarski-Class X,B )
A4: ex u being Element of Tarski-Class X st
( x = u & ex B being Ordinal st
( B in A & u in Tarski-Class X,B ) ) by A2, A3;
thus ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) by A4; :: thesis: verum

end;

given B being Ordinal such that A5: B in A and
A6: x in Tarski-Class X,B ; :: thesis: x in Tarski-Class X,A
reconsider u = x as Element of Tarski-Class X by A6;
A7: u in { v where v is Element of Tarski-Class X : ex B being Ordinal st
( B in A & v in Tarski-Class X,B ) } by A5, A6;
thus x in Tarski-Class X,A by A1, A7, Th12; :: thesis: verum