let n be Element of NAT ; :: thesis: for V being Subset of
for A being Subset of st A = V holds
( A is open iff V is open )
let V be Subset of ; :: thesis: for A being Subset of st A = V holds
( A is open iff V is open )
let A be Subset of ; :: 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 Th102, PRE_TOPC:def 5; :: thesis: verum