let T1, T2 be Universe; :: thesis: ( X c= T1 & ( for Y being Universe st X c= Y holds
T1 c= Y ) & X c= T2 & ( for Y being Universe st X c= Y holds
T2 c= Y ) implies T1 = T2 )
assume A1: ( X c= T1 & ( for Y being Universe st X c= Y holds
T1 c= Y ) & X c= T2 & ( for Y being Universe st X c= Y holds
T2 c= Y ) & not T1 = T2 ) ; :: thesis: contradiction
then ( T1 c= T2 & T2 c= T1 ) ;
hence contradiction by A1, XBOOLE_0:def 10; :: thesis: verum