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

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