let n be Element of NAT ; :: thesis: for A being Subset of (COMPLEX n) st A = {} holds
A is open
let A be Subset of (COMPLEX n); :: thesis: ( A = {} implies A is open )
assume A1: A = {} ; :: thesis: A is open
let x be Element of COMPLEX n; :: according to SEQ_4:def 14 :: thesis: ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) )
thus ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) ) by A1; :: thesis: verum