let X be set ; :: thesis: ( X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} implies X <> REAL )
assume A1: X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} ; :: thesis: X <> REAL
per cases ( X = Cl KurExSet or X = Cl (Int KurExSet) or X = Cl (Int (Cl KurExSet)) ) by A1, ENUMSET1:def 1;
suppose A2: X = Cl KurExSet ; :: thesis: X <> REAL
A3: 0 in REAL by XREAL_0:def 1;
( not 0 in {1} & not 0 in [.2,+infty.[ ) by XXREAL_1:236, TARSKI:def 1;
hence X <> REAL by A2, Th10, XBOOLE_0:def 3, A3; :: thesis: verum
end;
suppose X = Cl (Int KurExSet) ; :: thesis: X <> REAL
hence X <> REAL by Th24, BORSUK_5:46; :: thesis: verum
end;
suppose X = Cl (Int (Cl KurExSet)) ; :: thesis: X <> REAL
hence X <> REAL by Th27, BORSUK_5:46; :: thesis: verum
end;
end;