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