set A = KurExSet ;
A1:
Cl ((Cl ((Cl (KurExSet ` )) ` )) ` ) = ].-infty ,4.]
by Th22, BORSUK_5:77;
5 in {5}
by TARSKI:def 1;
then
5 in Cl (KurExSet ` )
by Th19, 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 Th23, XXREAL_1:234, XXREAL_1:236;
then A3:
Cl KurExSet <> Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )
by Th12, XBOOLE_0:def 3;
( not 5 in Cl ((Cl ((Cl (KurExSet ` )) ` )) ` ) & Cl ((Cl (KurExSet ` )) ` ) = [.4,+infty .[ )
by Th20, Th23, BORSUK_5:81, XXREAL_1:234;
then A4:
Cl ((Cl (KurExSet ` )) ` ) <> Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )
by XXREAL_1:236;
5 in Cl ((Cl ((Cl KurExSet ) ` )) ` )
by Th16, XXREAL_1:236;
then A5:
Cl ((Cl ((Cl KurExSet ) ` )) ` ) <> Cl ((Cl ((Cl (KurExSet ` )) ` )) ` )
by Th23, 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 Th19, XBOOLE_0:def 3;
Cl ((Cl ((Cl KurExSet ) ` )) ` ) = [.2,+infty .[
by Th15, BORSUK_5:75;
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 Th16, TOPS_1:def 1, XXREAL_1:236;
A9:
not 4 in Cl ((Cl KurExSet ) ` )
by Th14, 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_different
by A9, A3, A7, A5, A8, A2, A4, Th31, Th33, ZFMISC_1:def 8;
hence
card (Kurat14ClPart KurExSet ) = 6
by BORSUK_5:4; verum