let n be Element of NAT ; :: thesis: for V being Subset of (the_Complex_Space n)
for A being Subset of (COMPLEX n) st A = V holds
( A is open iff V is open )
let V be Subset of (the_Complex_Space n); :: thesis: for A being Subset of (COMPLEX n) st A = V holds
( A is open iff V is open )
let A be Subset of (COMPLEX n); :: thesis: ( A = V implies ( A is open iff V is open ) )
assume A = V ; :: thesis: ( A is open iff V is open )
then ( A in ComplexOpenSets n iff V in the topology of (the_Complex_Space n) ) ;
hence ( A is open iff V is open ) by SEQ_4:148, PRE_TOPC:def 5; :: thesis: verum