set A = KurExSet ;
KurExSet , Int KurExSet, Cl KurExSet, Int (Cl KurExSet), Cl (Int KurExSet), Cl (Int (Cl KurExSet)), Int (Cl (Int KurExSet)) are_mutually_distinct by Th54;
hence card (Kurat7Set KurExSet) = 7 by BORSUK_5:4; :: thesis: verum