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 Th18, 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 Th26; :: 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 Th25; :: thesis: verum
end;
end;