let M1, M2 be Cardinal; :: thesis: ( card X in M1 & ( for M being Cardinal st card X in M holds
M1 c= M ) & card X in M2 & ( for M being Cardinal st card X in M holds
M2 c= M ) implies M1 = M2 )
assume ( card X in M1 & ( for M being Cardinal st card X in M holds
M1 c= M ) & card X in M2 & ( for M being Cardinal st card X in M holds
M2 c= M ) ) ; :: thesis: M1 = M2
then ( M1 c= M2 & M2 c= M1 ) ;
hence M1 = M2 by XBOOLE_0:def 10; :: thesis: verum