set A = KurExSet ;
assume A2: the carrier of R^1 in Kurat14OpPart 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 A2, ENUMSET1:def 4, TOPMETR:24;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;