defpred S₁[ Ordinal] means ( M is_cofinal_with $1 & $1 is Cardinal );
A1: ex A being Ordinal st S₁[A] ;
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);
reconsider K = A as Cardinal by A2;
take K ; :: thesis: ( M is_cofinal_with K & ( for N being Cardinal st M is_cofinal_with N holds
K c= N ) )
thus M is_cofinal_with K by A2; :: thesis: for N being Cardinal st M is_cofinal_with N holds
K c= N
let N be Cardinal; :: thesis: ( M is_cofinal_with N implies K c= N )
assume M is_cofinal_with N ; :: thesis: K c= N
hence K c= N by A2; :: thesis: verum