set A = KurExSet ;
assume A1: the carrier of R^1 in Kurat14ClPart KurExSet ; :: according to SETFAM_1:def 12 :: 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:17;

suppose REAL = Cl KurExSet ; :: thesis: contradiction

hence contradiction by Th10, BORSUK_5:69; :: thesis: verum

end;

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

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

end;

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

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

end;

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

hence contradiction by Th17, BORSUK_5:70; :: thesis: verum

end;

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

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

end;

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

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

end;

end;