let X be non empty TopSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum