let n be Element of NAT ; :: thesis: for A, B being Subset of (COMPLEX n) st A is open & B is open holds
for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
let A, B be Subset of (COMPLEX n); :: thesis: ( A is open & B is open implies for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open )
assume A1: ( A is open & B is open ) ; :: thesis: for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
let C be Subset of (COMPLEX n); :: thesis: ( C = A /\ B implies C is open )
assume A2: C = A /\ B ; :: thesis: C is open
let x be Element of COMPLEX n; :: according to COMPLSP1:def 15 :: thesis: ( x in C implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in C ) ) )
assume A3: x in C ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in C ) )
then x in A by A2, XBOOLE_0:def 4;
then consider r1 being Real such that
A4: 0 < r1 and
A5: for z being Element of COMPLEX n st |.z.| < r1 holds
x + z in A by A1, Def15;
x in B by A2, A3, XBOOLE_0:def 4;
then consider r2 being Real such that
A6: 0 < r2 and
A7: for z being Element of COMPLEX n st |.z.| < r2 holds
x + z in B by A1, Def15;
take min r1,r2 ; :: thesis: ( 0 < min r1,r2 & ( for z being Element of COMPLEX n st |.z.| < min r1,r2 holds
x + z in C ) )
thus 0 < min r1,r2 by A4, A6, XXREAL_0:15; :: thesis: for z being Element of COMPLEX n st |.z.| < min r1,r2 holds
x + z in C
let z be Element of COMPLEX n; :: thesis: ( |.z.| < min r1,r2 implies x + z in C )
A8: ( min r1,r2 <= r1 & min r1,r2 <= r2 ) by XXREAL_0:17;
assume |.z.| < min r1,r2 ; :: thesis: x + z in C
then ( |.z.| < r1 & |.z.| < r2 ) by A8, XXREAL_0:2;
then ( x + z in A & x + z in B ) by A5, A7;
hence x + z in C by A2, XBOOLE_0:def 4; :: thesis: verum