let X, x be set ; 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; ( 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 )
; ( 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 Th9;
thus
( x in Tarski-Class (X,A) implies ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )
( ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) implies x in Tarski-Class (X,A) )
given B being Ordinal such that A3:
B in A
and
A4:
x in Tarski-Class (X,B)
; x in Tarski-Class (X,A)
reconsider u = x as Element of Tarski-Class X by A4;
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, A4;
hence
x in Tarski-Class (X,A)
by A1, Th9; verum