Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)), KurExSet are_mutually_different by Th55, Th56, BORSUK_5:7;
hence KurExSet , Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different by BORSUK_5:8; :: thesis: verum