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

X is closed

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

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

then ex Z being Subset of T st

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

hence X is closed ; :: thesis: verum

X is closed

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

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

then ex Z being Subset of T st

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

hence X is closed ; :: thesis: verum