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