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 that
A5: ( card X in M1 & ( for M being Cardinal st card X in M holds
M1 c= M ) ) and
A6: ( card X in M2 & ( for M being Cardinal st card X in M holds
M2 c= M ) ) ; :: thesis: M1 = M2
( M1 c= M2 & M2 c= M1 ) by A5, A6;
hence M1 = M2 by XBOOLE_0:def 10; :: thesis: verum