let X be set ; :: thesis: ( X in {(Int KurExSet ),(Int (Cl KurExSet )),(Int (Cl (Int KurExSet )))} implies X is non empty open Subset of R^1 )
assume A1: X in {(Int KurExSet ),(Int (Cl KurExSet )),(Int (Cl (Int KurExSet )))} ; :: thesis: X is non empty open Subset of R^1

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 is non empty open Subset of R^1

hence X is non empty open Subset of R^1 by Th20, TOPS_1:def 1; :: thesis: verum

end;

suppose X = Int (Cl KurExSet ) ; :: thesis: X is non empty open Subset of R^1

hence X is non empty open Subset of R^1 by Th28; :: thesis: verum

end;

suppose X = Int (Cl (Int KurExSet )) ; :: thesis: X is non empty open Subset of R^1

hence X is non empty open Subset of R^1 by Th27; :: thesis: verum

end;

end;