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 X = Int KurExSet ; :: thesis: X <> REAL

hence X <> REAL by Th25, XXREAL_1:205; :: thesis: verum

end;

suppose X = Int (Cl KurExSet ) ; :: thesis: X <> REAL

hence X <> REAL by Th28, BORSUK_5:71; :: thesis: verum

end;

suppose X = Int (Cl (Int KurExSet )) ; :: thesis: X <> REAL

hence X <> REAL by Th27, BORSUK_5:71; :: thesis: verum

end;

end;