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 Th10, Th22, BORSUK_5:63, 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 Th14, TOPMETR:17, XXREAL_1:224, XXREAL_1:294;
6 in ].5,+infty.[
by XXREAL_1:235;
then
6 in (Cl (KurExSet `)) `
by Th18, XBOOLE_0:def 3;
then A4:
(Cl ((Cl ((Cl KurExSet) `)) `)) ` <> (Cl (KurExSet `)) `
by A3, XXREAL_1:233;
A5:
4 in (Cl ((Cl KurExSet) `)) `
by Th13, 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 Th18, XBOOLE_0:def 3;
(Cl KurExSet) ` <> (Cl (Int (Cl KurExSet))) `
by Th29, BORSUK_5:71;
then A7:
(Cl KurExSet) ` <> (Cl ((Cl ((Cl KurExSet) `)) `)) `
by TOPS_1:def 1;
A8:
not 5 in (Cl ((Cl (KurExSet `)) `)) `
by Th20, XXREAL_1:233;
(Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` = ].4,+infty.[
by Th21, TOPMETR:17, 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 Th31, BORSUK_5:71;
A11:
( not 5 in (Cl ((Cl ((Cl KurExSet) `)) `)) ` & 5 in (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` )
by Th15, Th22, 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_distinct
by A2, A7, A9, A4, A10, A6, A11, A8;
hence
card (Kurat14OpPart KurExSet) = 6
by BORSUK_5:3; verum