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 closed iff V is closed )
let V be Subset of (the_Complex_Space n); :: thesis: for A being Subset of (COMPLEX n) st A = V holds
( A is closed iff V is closed )
let A be Subset of (COMPLEX n); :: thesis: ( A = V implies ( A is closed iff V is closed ) )
assume A = V ; :: thesis: ( A is closed iff V is closed )
then ( ([#] (the_Complex_Space n)) \ V is open iff A ` is open ) by Th4;
hence ( A is closed iff V is closed ) by SEQ_4:132; :: thesis: verum