set A = the Ordinal;
defpred S₁[ Ordinal] means c₁, the Ordinal are_equipotent ;
A1: ex A being Ordinal st S₁[A] ;
consider B being Ordinal such that
A2: ( S₁[B] & ( for C being Ordinal st S₁[C] holds
B c= C ) ) from ORDINAL1:sch 1(A1);
reconsider IT = B as set ;
take IT ; :: thesis: IT is cardinal
take B ; :: according to CARD_1:def 1 :: thesis: ( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) )
thus ( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) by A2, WELLORD2:15; :: thesis: verum