let X be LinearTopSpace; for A, B being Subset of X holds (Cl A) + (Cl B) c= Cl (A + B)
let A, B be Subset of X; (Cl A) + (Cl B) c= Cl (A + B)
let z be object ; TARSKI:def 3 ( not z in (Cl A) + (Cl B) or z in Cl (A + B) )
assume A1:
z in (Cl A) + (Cl B)
; z in Cl (A + B)
then reconsider z = z as Point of X ;
{ (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 9;
then consider a, b being Point of X such that
A2:
z = a + b
and
A3:
a in Cl A
and
A4:
b in Cl B
by A1;
now for W being Subset of X st W is open & z in W holds
A + B meets Wlet W be
Subset of
X;
( W is open & z in W implies A + B meets W )assume that A5:
W is
open
and A6:
z in W
;
A + B meets W
W is
a_neighborhood of
z
by A5, A6, CONNSP_2:3;
then consider W1 being
a_neighborhood of
a,
W2 being
a_neighborhood of
b such that A7:
W1 + W2 c= W
by A2, Th31;
a in Int W1
by CONNSP_2:def 1;
then
A meets Int W1
by A3, TOPS_1:12;
then consider x being
object such that A8:
x in A
and A9:
x in Int W1
by XBOOLE_0:3;
reconsider x =
x as
Point of
X by A8;
A10:
(Int W1) + (Int W2) c= Int W
by A7, Th36;
b in Int W2
by CONNSP_2:def 1;
then
B meets Int W2
by A4, TOPS_1:12;
then consider y being
object 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;
(
x + y in A + B &
x + y in (Int W1) + (Int W2) )
by A8, A9, A11, A12, Th3;
then
A + B meets Int W
by A10, XBOOLE_0:3;
hence
A + B meets W
by A5, TOPS_1:23;
verum end;
hence
z in Cl (A + B)
by TOPS_1:12; verum