let T be non empty TopSpace; :: thesis: for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T

let x be Element of OpenClosedSet T; :: thesis: x ` is Element of OpenClosedSet T

reconsider y = x as Subset of T ;

A1: y is open by Th1;

y is closed by Th2;

then A2: x ` is open ;

x ` is closed by A1;

hence x ` is Element of OpenClosedSet T by A2, Th3; :: thesis: verum

let x be Element of OpenClosedSet T; :: thesis: x ` is Element of OpenClosedSet T

reconsider y = x as Subset of T ;

A1: y is open by Th1;

y is closed by Th2;

then A2: x ` is open ;

x ` is closed by A1;

hence x ` is Element of OpenClosedSet T by A2, Th3; :: thesis: verum