set A = KurExSet ;
assume A1: the carrier of R^1 in Kurat14ClPart KurExSet ; :: according to SETFAM_1:def 13 :: thesis: contradiction

per cases ( REAL = Cl KurExSet or REAL = Cl ((Cl KurExSet ) ` ) or REAL = Cl ((Cl ((Cl KurExSet ) ` )) ` ) or REAL = Cl (KurExSet ` ) or REAL = Cl ((Cl (KurExSet ` )) ` ) or REAL = Cl ((Cl ((Cl (KurExSet ` )) ` )) ` ) ) by A1, ENUMSET1:def 4, TOPMETR:24;

suppose REAL = Cl KurExSet ; :: thesis: contradiction

hence contradiction by Th12, BORSUK_5:103; :: thesis: verum

end;

suppose REAL = Cl ((Cl KurExSet ) ` ) ; :: thesis: contradiction

hence contradiction by Th14, BORSUK_5:73; :: thesis: verum

end;

suppose REAL = Cl ((Cl ((Cl KurExSet ) ` )) ` ) ; :: thesis: contradiction

hence contradiction by Th16, BORSUK_5:72; :: thesis: verum

end;

suppose REAL = Cl (KurExSet ` ) ; :: thesis: contradiction

hence contradiction by Th19, BORSUK_5:104; :: thesis: verum

end;

suppose REAL = Cl ((Cl (KurExSet ` )) ` ) ; :: thesis: contradiction

hence contradiction by Th21, BORSUK_5:72; :: thesis: verum

end;

suppose REAL = Cl ((Cl ((Cl (KurExSet ` )) ` )) ` ) ; :: thesis: contradiction

hence contradiction by Th23, BORSUK_5:73; :: thesis: verum

end;

end;