let T be non empty TopSpace; :: thesis: for X being Subset of T st X in OpenClosedSet T holds

X is open

let X be Subset of T; :: thesis: ( X in OpenClosedSet T implies X is open )

assume X in OpenClosedSet T ; :: thesis: X is open

then ex Z being Subset of T st

( Z = X & Z is open & Z is closed ) ;

hence X is open ; :: thesis: verum

X is open

let X be Subset of T; :: thesis: ( X in OpenClosedSet T implies X is open )

assume X in OpenClosedSet T ; :: thesis: X is open

then ex Z being Subset of T st

( Z = X & Z is open & Z is closed ) ;

hence X is open ; :: thesis: verum