let M1, M2 be cardinal number ; :: thesis: ( ex A being Subset of T st
( A is dense & M1 = card A ) & ( for B being Subset of T st B is dense holds
M1 c= card B ) & ex A being Subset of T st
( A is dense & M2 = card A ) & ( for B being Subset of T st B is dense holds
M2 c= card B ) implies M1 = M2 )
assume ( ex B being Subset of T st
( B is dense & M1 = card B ) & ( for B being Subset of T st B is dense holds
M1 c= card B ) & ex B being Subset of T st
( B is dense & M2 = card B ) & ( for B being Subset of T st B is dense holds
M2 c= card B ) ) ; :: thesis: M1 = M2
hence ( M1 c= M2 & M2 c= M1 ) ; :: according to XBOOLE_0:def 10 :: thesis: verum