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 F1 being Subset of X1
for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds
ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 )

let X1, X2 be non empty SubSpace of X; :: thesis: for x being Point of (X1 union X2)
for F1 being Subset of X1
for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds
ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 )

let x be Point of (X1 union X2); :: thesis: for F1 being Subset of X1
for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds
ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 )

let F1 be Subset of X1; :: thesis: for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds
ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 )

let F2 be Subset of X2; :: thesis: ( F1 is closed & x in F1 & F2 is closed & x in F2 implies ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 ) )

assume that
A1: F1 is closed and
A2: x in F1 and
A3: F2 is closed and
A4: x in F2 ; :: thesis: ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 )

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 H1 being Subset of (X1 union X2) such that
A6: H1 is closed and
A7: H1 /\ ([#] X1) = F1 by ;
A8: x in H1 by ;
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 H2 being Subset of (X1 union X2) such that
A10: H2 is closed and
A11: H2 /\ ([#] X2) = F2 by ;
A12: x in H2 by ;
take H = H1 /\ H2; :: thesis: ( H is closed & x in H & H c= F1 \/ F2 )
A13: ( H /\ C1 c= H1 /\ C1 & H /\ C2 c= H2 /\ C2 ) by ;
the carrier of (X1 union X2) = C1 \/ C2 by TSEP_1:def 2;
then H = H /\ (C1 \/ C2) by XBOOLE_1:28
.= (H /\ C1) \/ (H /\ C2) by XBOOLE_1:23 ;
hence ( H is closed & x in H & H c= F1 \/ F2 ) by ; :: thesis: verum