set A = KurExSet ;
A1: (Cl KurExSet ) ` = ].-infty ,1.[ \/ ].1,2.[ by Th12, BORSUK_5:95;
A2: (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` = ].-infty ,2.[ by Th16, TOPMETR:24, XXREAL_1:224, XXREAL_1:294;
A3: (Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` = ].4,+infty .[ by Th23, TOPMETR:24, XXREAL_1:224, XXREAL_1:288;
A4: 4 in (Cl ((Cl KurExSet ) ` )) ` by Th15, XXREAL_1:235;
6 in ].5,+infty .[ by XXREAL_1:235;
then A5: 6 in (Cl (KurExSet ` )) ` by Th20, XBOOLE_0:def 3;
A6: 5 in (Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` by Th24, XXREAL_1:235;
( not 5 in ].-infty ,1.[ & not 5 in ].1,2.[ ) by XXREAL_1:4;
then A7: (Cl KurExSet ) ` <> (Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` by A1, A6, XBOOLE_0:def 3;
(Cl KurExSet ) ` <> (Cl (Int (Cl KurExSet ))) ` by Th31, BORSUK_5:105;
then A8: (Cl KurExSet ) ` <> (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` by TOPS_1:def 1;
A9: (Cl ((Cl KurExSet ) ` )) ` <> (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` by A2, A4, XXREAL_1:233;
A10: (Cl ((Cl KurExSet ) ` )) ` <> (Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` by A3, A4, XXREAL_1:235;
A11: (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` <> (Cl (KurExSet ` )) ` by A2, A5, XXREAL_1:233;
A12: not 5 in (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` by Th17, XXREAL_1:233;
( (Cl (Int (Cl KurExSet ))) ` = (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` & (Cl (Int KurExSet )) ` = (Cl ((Cl (KurExSet ` )) ` )) ` ) by TOPS_1:def 1;
then A13: (Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` <> (Cl ((Cl (KurExSet ` )) ` )) ` by Th33, BORSUK_5:105;
A14: not 5 in ].4,5.[ by XXREAL_1:4;
not 5 in ].5,+infty .[ by XXREAL_1:235;
then A15: not 5 in (Cl (KurExSet ` )) ` by A14, Th20, XBOOLE_0:def 3;
A16: 5 in (Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` by Th24, XXREAL_1:235;
not 5 in (Cl ((Cl (KurExSet ` )) ` )) ` by Th22, XXREAL_1:233;
then (Cl KurExSet ) ` ,(Cl ((Cl KurExSet ) ` )) ` ,(Cl ((Cl ((Cl KurExSet ) ` )) ` )) ` ,(Cl (KurExSet ` )) ` ,(Cl ((Cl (KurExSet ` )) ` )) ` ,(Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )) ` are_mutually_different by A7, A8, A9, A10, A11, A12, A13, A15, A16, ZFMISC_1:def 8;
hence card (Kurat14OpPart KurExSet ) = 6 by BORSUK_5:4; :: thesis: verum