set A = KurExSet ;
KurExSet , Int KurExSet , Cl KurExSet , Int (Cl KurExSet ), Cl (Int KurExSet ), Cl (Int (Cl KurExSet )), Int (Cl (Int KurExSet )) are_mutually_different by Th57, BORSUK_5:10;
hence card (Kurat7Set KurExSet ) = 7 by BORSUK_5:5; :: thesis: verum