let A, B be Ordinal; :: thesis: ( UNIVERSE A = UNIVERSE B implies A = B )
assume that
A1: UNIVERSE A = UNIVERSE B and
A2: A <> B ; :: thesis: contradiction
( A in B or B in A ) by A2, ORDINAL1:14;
then ( UNIVERSE A in UNIVERSE B or UNIVERSE B in UNIVERSE A ) by Th70;
hence contradiction by A1; :: thesis: verum