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 Th22;
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:7; :: thesis: verum