let K1, K2 be Cardinal; :: thesis: ( M is_cofinal_with K1 & ( for N being Cardinal st M is_cofinal_with N holds
K1 c= N ) & M is_cofinal_with K2 & ( for N being Cardinal st M is_cofinal_with N holds
K2 c= N ) implies K1 = K2 )
assume ( M is_cofinal_with K1 & ( for N being Cardinal st M is_cofinal_with N holds
K1 c= N ) & M is_cofinal_with K2 & ( for N being Cardinal st M is_cofinal_with N holds
K2 c= N ) ) ; :: thesis: K1 = K2
then ( K1 c= K2 & K2 c= K1 ) ;
hence K1 = K2 by XBOOLE_0:def 10; :: thesis: verum