defpred S₁[ Ordinal] means $1,X are_equipotent ;
A1: ex A being Ordinal st S₁[A] by Th4;
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);
A is cardinal

proof

take A ; :: according to CARD_1:def 1 :: thesis: ( A = A & ( for A being Ordinal st A,A are_equipotent holds
A c= A ) )
thus A = A ; :: thesis: for A being Ordinal st A,A are_equipotent holds
A c= A
let B be Ordinal; :: thesis: ( B,A are_equipotent implies A c= B )
assume B,A are_equipotent ; :: thesis: A c= B
hence A c= B by A2, WELLORD2:15; :: thesis: verum

end;

then reconsider M = A as Cardinal ;
take M ; :: thesis: X,M are_equipotent
thus X,M are_equipotent by A2; :: thesis: verum