let n be 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 that
A1: A is open and
A2: 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 A3: C = A /\ B ; :: thesis: C is open
let x be Element of COMPLEX n; :: according to SEQ_4:def 14 :: 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 A4: 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 A3, XBOOLE_0:def 4;
then consider r1 being Real such that
A5: 0 < r1 and
A6: for z being Element of COMPLEX n st |.z.| < r1 holds
x + z in A by A1;
x in B by A3, A4, XBOOLE_0:def 4;
then consider r2 being Real such that
A7: 0 < r2 and
A8: for z being Element of COMPLEX n st |.z.| < r2 holds
x + z in B by A2;
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 A5, A7, 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 )
assume A9: |.z.| < min (r1,r2) ; :: thesis: x + z in C
min (r1,r2) <= r2 by XXREAL_0:17;
then |.z.| < r2 by A9, XXREAL_0:2;
then A10: x + z in B by A8;
min (r1,r2) <= r1 by XXREAL_0:17;
then |.z.| < r1 by A9, XXREAL_0:2;
then x + z in A by A6;
hence x + z in C by A3, A10, XBOOLE_0:def 4; :: thesis: verum