theorem :: CLASSES2:72

for A, B being Ordinal holds
( A c= B iff UNIVERSE A c= UNIVERSE B )