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 ) )
then 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 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 x in Tarski-Class X,A ; :: thesis: ex B being Ordinal st
( B in A & x in Tarski-Class X,B )
then 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;
hence ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) ; :: thesis: verum

end;

given B being Ordinal such that A3: ( B in A & x in Tarski-Class X,B ) ; :: thesis: x in Tarski-Class X,A
reconsider u = x as Element of Tarski-Class X by A3;
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 A3;
hence x in Tarski-Class X,A by A1, Th12; :: thesis: verum