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 U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let X1, X2 be non empty SubSpace of X; :: thesis: for x being Point of (X1 union X2)

for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let x be Point of (X1 union X2); :: thesis: for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let U1 be Subset of X1; :: thesis: for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let U2 be Subset of X2; :: thesis: ( U1 is open & x in U1 & U2 is open & x in U2 implies ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 ) )

assume that

A1: U1 is open and

A2: x in U1 and

A3: U2 is open and

A4: x in U2 ; :: thesis: ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

A5: X1 is SubSpace of X1 union X2 by TSEP_1:22;

then reconsider C1 = the carrier of X1 as Subset of (X1 union X2) by TSEP_1:1;

consider V1 being Subset of (X1 union X2) such that

A6: V1 is open and

A7: V1 /\ ([#] X1) = U1 by A1, A5, TOPS_2:24;

A8: x in V1 by A2, A7, XBOOLE_0:def 4;

A9: X2 is SubSpace of X1 union X2 by TSEP_1:22;

then reconsider C2 = the carrier of X2 as Subset of (X1 union X2) by TSEP_1:1;

consider V2 being Subset of (X1 union X2) such that

A10: V2 is open and

A11: V2 /\ ([#] X2) = U2 by A3, A9, TOPS_2:24;

A12: x in V2 by A4, A11, XBOOLE_0:def 4;

take V = V1 /\ V2; :: thesis: ( V is open & x in V & V c= U1 \/ U2 )

A13: ( V /\ C1 c= V1 /\ C1 & V /\ C2 c= V2 /\ C2 ) by XBOOLE_1:17, XBOOLE_1:26;

the carrier of (X1 union X2) = C1 \/ C2 by TSEP_1:def 2;

then V = V /\ (C1 \/ C2) by XBOOLE_1:28

.= (V /\ C1) \/ (V /\ C2) by XBOOLE_1:23 ;

hence ( V is open & x in V & V c= U1 \/ U2 ) by A6, A7, A10, A11, A13, A8, A12, XBOOLE_0:def 4, XBOOLE_1:13; :: thesis: verum

for x being Point of (X1 union X2)

for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let X1, X2 be non empty SubSpace of X; :: thesis: for x being Point of (X1 union X2)

for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let x be Point of (X1 union X2); :: thesis: for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let U1 be Subset of X1; :: thesis: for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

let U2 be Subset of X2; :: thesis: ( U1 is open & x in U1 & U2 is open & x in U2 implies ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 ) )

assume that

A1: U1 is open and

A2: x in U1 and

A3: U2 is open and

A4: x in U2 ; :: thesis: ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

A5: X1 is SubSpace of X1 union X2 by TSEP_1:22;

then reconsider C1 = the carrier of X1 as Subset of (X1 union X2) by TSEP_1:1;

consider V1 being Subset of (X1 union X2) such that

A6: V1 is open and

A7: V1 /\ ([#] X1) = U1 by A1, A5, TOPS_2:24;

A8: x in V1 by A2, A7, XBOOLE_0:def 4;

A9: X2 is SubSpace of X1 union X2 by TSEP_1:22;

then reconsider C2 = the carrier of X2 as Subset of (X1 union X2) by TSEP_1:1;

consider V2 being Subset of (X1 union X2) such that

A10: V2 is open and

A11: V2 /\ ([#] X2) = U2 by A3, A9, TOPS_2:24;

A12: x in V2 by A4, A11, XBOOLE_0:def 4;

take V = V1 /\ V2; :: thesis: ( V is open & x in V & V c= U1 \/ U2 )

A13: ( V /\ C1 c= V1 /\ C1 & V /\ C2 c= V2 /\ C2 ) by XBOOLE_1:17, XBOOLE_1:26;

the carrier of (X1 union X2) = C1 \/ C2 by TSEP_1:def 2;

then V = V /\ (C1 \/ C2) by XBOOLE_1:28

.= (V /\ C1) \/ (V /\ C2) by XBOOLE_1:23 ;

hence ( V is open & x in V & V c= U1 \/ U2 ) by A6, A7, A10, A11, A13, A8, A12, XBOOLE_0:def 4, XBOOLE_1:13; :: thesis: verum