let X be LinearTopSpace; for x1, x2 being Point of X
for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
let x1, x2 be Point of X; for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
let V be a_neighborhood of x1 + x2; ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
x1 + x2 in Int V
by CONNSP_2:def 1;
then consider V1, V2 being Subset of X such that
A1:
V1 is open
and
A2:
V2 is open
and
A3:
x1 in V1
and
A4:
x2 in V2
and
A5:
V1 + V2 c= Int V
by Def8;
Int V2 = V2
by A2, TOPS_1:23;
then reconsider V2 = V2 as a_neighborhood of x2 by A4, CONNSP_2:def 1;
Int V1 = V1
by A1, TOPS_1:23;
then reconsider V1 = V1 as a_neighborhood of x1 by A3, CONNSP_2:def 1;
take
V1
; ex V2 being a_neighborhood of x2 st V1 + V2 c= V
take
V2
; V1 + V2 c= V
Int V c= V
by TOPS_1:16;
hence
V1 + V2 c= V
by A5; verum