let X be set ; :: thesis: ex A being Ordinal st
( Tarski-Class (X,A) = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X ) )
defpred S₁[ Ordinal] means Tarski-Class (X,$1) = Tarski-Class X;
A1: ex A being Ordinal st S₁[A] by Th19;
consider A being Ordinal such that
A2: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A1);
take A ; :: thesis: ( Tarski-Class (X,A) = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X ) )
thus Tarski-Class (X,A) = Tarski-Class X by A2; :: thesis: for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X
let B be Ordinal; :: thesis: ( B in A implies Tarski-Class (X,B) <> Tarski-Class X )
assume B in A ; :: thesis: Tarski-Class (X,B) <> Tarski-Class X
hence Tarski-Class (X,B) <> Tarski-Class X by A2, ORDINAL1:5; :: thesis: verum