let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 holds
X1 meet X2 is SubSpace of X0
let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 )
assume A1: X1 meets X2 ; :: thesis: ( not X1 is SubSpace of X0 or not X2 is SubSpace of X0 or X1 meet X2 is SubSpace of X0 )
assume ( X1 is SubSpace of X0 & X2 is SubSpace of X0 ) ; :: thesis: X1 meet X2 is SubSpace of X0
then ( the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 ) by TSEP_1:4;
then A2: the carrier of X1 \/ the carrier of X2 c= the carrier of X0 by XBOOLE_1:8;
the carrier of X1 /\ the carrier of X2 c= the carrier of X1 \/ the carrier of X2 by XBOOLE_1:29;
then the carrier of X1 /\ the carrier of X2 c= the carrier of X0 by A2, XBOOLE_1:1;
then the carrier of (X1 meet X2) c= the carrier of X0 by A1, TSEP_1:def 4;
hence X1 meet X2 is SubSpace of X0 by TSEP_1:4; :: thesis: verum