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