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;
assume A1: X0 meets X1 ; :: thesis: X0 meet X1 is open SubSpace of X1
reconsider B = A0 /\ A1 as Subset of X1 by XBOOLE_1:17;
( B = A0 /\ ([#] X1) & A0 is open ) by TSEP_1:16;
then ( B is open & B = the carrier of (X0 meet X1) & X0 meet X1 is SubSpace of X1 ) by A1, TOPS_2:32, TSEP_1:30, TSEP_1:def 5;
hence X0 meet X1 is open SubSpace of X1 by TSEP_1:16; :: thesis: verum