let n be Element of NAT ; :: thesis: for A being Subset of holds
( A in ComplexOpenSets n iff A is open )
let B be Subset of ; :: thesis: ( B in ComplexOpenSets n iff B is open )
( B in { A where A is Subset of : A is open } iff ex C being Subset of st
( B = C & C is open ) ) ;
hence ( B in ComplexOpenSets n iff B is open ) ; :: thesis: verum