let X be non empty TopSpace; :: thesis: for X1 being non empty SubSpace of X

for X0 being non empty closed SubSpace of X st X0 meets X1 holds

X0 meet X1 is closed SubSpace of X1

let X1 be non empty SubSpace of X; :: thesis: for X0 being non empty closed SubSpace of X st X0 meets X1 holds

X0 meet X1 is closed SubSpace of X1

let X0 be non empty closed SubSpace of X; :: thesis: ( X0 meets X1 implies X0 meet X1 is closed SubSpace of X1 )

reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;

reconsider B = A0 /\ A1 as Subset of X1 by XBOOLE_1:17;

( B = A0 /\ ([#] X1) & A0 is closed ) by TSEP_1:11;

then A1: B is closed by PRE_TOPC:13;

assume A2: X0 meets X1 ; :: thesis: X0 meet X1 is closed SubSpace of X1

then B = the carrier of (X0 meet X1) by TSEP_1:def 4;

hence X0 meet X1 is closed SubSpace of X1 by A2, A1, TSEP_1:11, TSEP_1:27; :: thesis: verum

for X0 being non empty closed SubSpace of X st X0 meets X1 holds

X0 meet X1 is closed SubSpace of X1

let X1 be non empty SubSpace of X; :: thesis: for X0 being non empty closed SubSpace of X st X0 meets X1 holds

X0 meet X1 is closed SubSpace of X1

let X0 be non empty closed SubSpace of X; :: thesis: ( X0 meets X1 implies X0 meet X1 is closed SubSpace of X1 )

reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;

reconsider B = A0 /\ A1 as Subset of X1 by XBOOLE_1:17;

( B = A0 /\ ([#] X1) & A0 is closed ) by TSEP_1:11;

then A1: B is closed by PRE_TOPC:13;

assume A2: X0 meets X1 ; :: thesis: X0 meet X1 is closed SubSpace of X1

then B = the carrier of (X0 meet X1) by TSEP_1:def 4;

hence X0 meet X1 is closed SubSpace of X1 by A2, A1, TSEP_1:11, TSEP_1:27; :: thesis: verum