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:8;
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:9; :: thesis: verum