let A, B be Ordinal; :: thesis: ( UNIVERSE A = UNIVERSE B implies A = B )
assume A1: ( UNIVERSE A = UNIVERSE B & A <> B ) ; :: thesis: contradiction
then ( A in B or B in A ) by ORDINAL1:24;
then ( UNIVERSE A in UNIVERSE B or UNIVERSE B in UNIVERSE A ) by Th80;
hence contradiction by A1; :: thesis: verum