let X be non empty TopSpace; :: thesis: for X1 being non empty SubSpace of X
for X0 being non empty open SubSpace of X st X0 meets X1 holds
X0 meet X1 is open SubSpace of X1
let X1 be non empty SubSpace of X; :: thesis: for X0 being non empty open SubSpace of X st X0 meets X1 holds
X0 meet X1 is open SubSpace of X1
let X0 be non empty open SubSpace of X; :: thesis: ( X0 meets X1 implies X0 meet X1 is open 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 open ) by TSEP_1:16;
then A1: B is open by TOPS_2:24;
assume A2: X0 meets X1 ; :: thesis: X0 meet X1 is open SubSpace of X1
then B = the carrier of (X0 meet X1) by TSEP_1:def 4;
hence X0 meet X1 is open SubSpace of X1 by A2, A1, TSEP_1:16, TSEP_1:27; :: thesis: verum