let X be set ; :: thesis: ( X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} implies X <> REAL )
assume A1: X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} ; :: thesis: X <> REAL
per cases ( X = Int KurExSet or X = Int (Cl KurExSet) or X = Int (Cl (Int KurExSet)) ) by A1, ENUMSET1:def 1;
suppose A2: X = Int KurExSet ; :: thesis: X <> REAL
5 in REAL by XREAL_0:def 1;
hence X <> REAL by Th23, XXREAL_1:205, A2; :: thesis: verum
end;
suppose X = Int (Cl KurExSet) ; :: thesis: X <> REAL
hence X <> REAL by Th26, BORSUK_5:45; :: thesis: verum
end;
suppose X = Int (Cl (Int KurExSet)) ; :: thesis: X <> REAL
hence X <> REAL by Th25, BORSUK_5:45; :: thesis: verum
end;
end;