let n be Element of NAT ; :: thesis: for V being Subset of
for A being Subset of st A = V holds
( A is closed iff V is closed )
let V be Subset of ; :: thesis: for A being Subset of st A = V holds
( A is closed iff V is closed )
let A be Subset of ; :: 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 Th108;
hence ( A is closed iff V is closed ) by Th109, PRE_TOPC:def 6; :: thesis: verum