let X be LinearTopSpace; :: thesis: for A, B being Subset of X holds (Cl A) + (Cl B) c= Cl (A + B)
let A, B be Subset of X; :: thesis: (Cl A) + (Cl B) c= Cl (A + B)
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (Cl A) + (Cl B) or z in Cl (A + B) )
A1:
{ (u + v) where u, v is Point of X : ( u in Cl A & v in Cl B ) } = (Cl A) + (Cl B)
by RUSUB_4:def 10;
assume A2:
z in (Cl A) + (Cl B)
; :: thesis: z in Cl (A + B)
then reconsider z = z as Point of X ;
consider a, b being Point of X such that
A3:
z = a + b
and
A4:
a in Cl A
and
A5:
b in Cl B
by A1, A2;
now let W be
Subset of
X;
:: thesis: ( W is open & z in W implies A + B meets W )assume that A6:
W is
open
and A7:
z in W
;
:: thesis: A + B meets W
W is
a_neighborhood of
z
by A6, A7, CONNSP_2:5;
then consider W1 being
a_neighborhood of
a,
W2 being
a_neighborhood of
b such that A8:
W1 + W2 c= W
by A3, Th32;
a in Int W1
by CONNSP_2:def 1;
then
A meets Int W1
by A4, TOPS_1:39;
then consider x being
set such that A9:
x in A
and A10:
x in Int W1
by XBOOLE_0:3;
reconsider x =
x as
Point of
X by A9;
b in Int W2
by CONNSP_2:def 1;
then
B meets Int W2
by A5, TOPS_1:39;
then consider y being
set such that A11:
y in B
and A12:
y in Int W2
by XBOOLE_0:3;
reconsider y =
y as
Point of
X by A11;
A13:
x + y in A + B
by A9, A11, Th3;
A14:
(Int W1) + (Int W2) c= Int W
by A8, Th37;
x + y in (Int W1) + (Int W2)
by A10, A12, Th3;
then
A + B meets Int W
by A13, A14, XBOOLE_0:3;
hence
A + B meets W
by A6, TOPS_1:55;
:: thesis: verum end;
hence
z in Cl (A + B)
by TOPS_1:39; :: thesis: verum