let n be Nat; :: thesis: for A being Subset of (COMPLEX n) st A = COMPLEX n holds
A is open
let A be Subset of (COMPLEX n); :: thesis: ( A = COMPLEX n implies A is open )
assume A1: A = COMPLEX n ; :: 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 ) ) )
assume x in A ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) )
reconsider j = 1 as Element of REAL by NUMBERS:19;
take j ; :: thesis: ( 0 < j & ( for z being Element of COMPLEX n st |.z.| < j holds
x + z in A ) )
thus 0 < j ; :: thesis: for z being Element of COMPLEX n st |.z.| < j holds
x + z in A
let z be Element of COMPLEX n; :: thesis: ( |.z.| < j implies x + z in A )
assume |.z.| < j ; :: thesis: x + z in A
thus x + z in A by A1; :: thesis: verum