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