theorem Th54: :: KURATO_1:54
KurExSet , Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_distinct by Th52;