let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for x1 being Point of X1
for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
let X1, X2 be non empty SubSpace of X; for x being Point of (X1 union X2)
for x1 being Point of X1
for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
let x be Point of (X1 union X2); for x1 being Point of X1
for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
let x1 be Point of X1; for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
let x2 be Point of X2; ( x1 = x & x2 = x implies for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 ) )
assume A1:
( x1 = x & x2 = x )
; for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
let A1 be a_neighborhood of x1; for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
let A2 be a_neighborhood of x2; ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
consider U1 being Subset of X1 such that
A2:
U1 is open
and
A3:
U1 c= A1
and
A4:
x1 in U1
by CONNSP_2:6;
consider U2 being Subset of X2 such that
A5:
U2 is open
and
A6:
U2 c= A2
and
A7:
x2 in U2
by CONNSP_2:6;
consider V being Subset of (X1 union X2) such that
A8:
( V is open & x in V & V c= U1 \/ U2 )
by A1, A2, A4, A5, A7, Th14;
take
V
; ( V is open & x in V & V c= A1 \/ A2 )
U1 \/ U2 c= A1 \/ A2
by A3, A6, XBOOLE_1:13;
hence
( V is open & x in V & V c= A1 \/ A2 )
by A8, XBOOLE_1:1; verum