set A = KurExSet ;
A1:
Cl ((Cl ((Cl (KurExSet `)) `)) `) = ].-infty,4.]
by Th20, BORSUK_5:51;
5 in {5}
by TARSKI:def 1;
then
5 in Cl (KurExSet `)
by Th17, XBOOLE_0:def 3;
then A2:
( Cl (Int KurExSet) = Cl ((Cl (KurExSet `)) `) & Cl (KurExSet `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `) )
by A1, TOPS_1:def 1, XXREAL_1:234;
( not 5 in Cl ((Cl ((Cl (KurExSet `)) `)) `) & 5 in [.2,+infty.[ )
by Th21, XXREAL_1:234, XXREAL_1:236;
then A3:
Cl KurExSet <> Cl ((Cl ((Cl (KurExSet `)) `)) `)
by Th10, XBOOLE_0:def 3;
( not 5 in Cl ((Cl ((Cl (KurExSet `)) `)) `) & Cl ((Cl (KurExSet `)) `) = [.4,+infty.[ )
by Th18, Th21, BORSUK_5:55, XXREAL_1:234;
then A4:
Cl ((Cl (KurExSet `)) `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `)
by XXREAL_1:236;
5 in Cl ((Cl ((Cl KurExSet) `)) `)
by Th14, XXREAL_1:236;
then A5:
Cl ((Cl ((Cl KurExSet) `)) `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `)
by Th21, XXREAL_1:234;
( not 6 in ].-infty,4.] & not 6 in {5} )
by TARSKI:def 1, XXREAL_1:234;
then A6:
not 6 in Cl (KurExSet `)
by Th17, XBOOLE_0:def 3;
Cl ((Cl ((Cl KurExSet) `)) `) = [.2,+infty.[
by Th13, BORSUK_5:49;
then A7:
Cl ((Cl ((Cl KurExSet) `)) `) <> Cl (KurExSet `)
by A6, XXREAL_1:236;
A8:
( 4 in Cl ((Cl ((Cl KurExSet) `)) `) & Cl (Int (Cl KurExSet)) = Cl ((Cl ((Cl KurExSet) `)) `) )
by Th14, TOPS_1:def 1, XXREAL_1:236;
A9:
not 4 in Cl ((Cl KurExSet) `)
by Th12, XXREAL_1:234;
then
Cl ((Cl KurExSet) `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `)
by A1, XXREAL_1:234;
then
Cl KurExSet, Cl ((Cl KurExSet) `), Cl ((Cl ((Cl KurExSet) `)) `), Cl (KurExSet `), Cl ((Cl (KurExSet `)) `), Cl ((Cl ((Cl (KurExSet `)) `)) `) are_mutually_distinct
by A9, A3, A7, A5, A8, A2, A4, Th29, Th31;
hence
card (Kurat14ClPart KurExSet) = 6
by BORSUK_5:3; verum