let A, B be Ordinal; :: thesis: ( A c= B iff UNIVERSE A c= UNIVERSE B )
thus ( A c= B implies UNIVERSE A c= UNIVERSE B ) :: thesis: ( UNIVERSE A c= UNIVERSE B implies A c= B )
proof
assume A1: A c= B ; :: thesis: UNIVERSE A c= UNIVERSE B
assume not UNIVERSE A c= UNIVERSE B ; :: thesis: contradiction
then UNIVERSE B in UNIVERSE A by Th53;
then B in A by Th70;
hence contradiction by A1, ORDINAL1:5; :: thesis: verum
end;
assume A2: UNIVERSE A c= UNIVERSE B ; :: thesis: A c= B
assume not A c= B ; :: thesis: contradiction
then B in A by ORDINAL1:16;
then UNIVERSE B in UNIVERSE A by Th70;
hence contradiction by A2, ORDINAL1:5; :: thesis: verum