let X be non empty TopSpace; :: thesis: for Y1, Y2, X1, X2 being non empty SubSpace of X st Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds
Y1 meet Y2 is SubSpace of X1 meet X2
let Y1, Y2, X1, X2 be non empty SubSpace of X; :: thesis: ( Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies Y1 meet Y2 is SubSpace of X1 meet X2 )
assume A1: Y1 meets Y2 ; :: thesis: ( not Y1 is SubSpace of X1 or not Y2 is SubSpace of X2 or Y1 meet Y2 is SubSpace of X1 meet X2 )
assume ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 ) ; :: thesis: Y1 meet Y2 is SubSpace of X1 meet X2
then A2: ( the carrier of Y1 c= the carrier of X1 & the carrier of Y2 c= the carrier of X2 ) by TSEP_1:4;
then A3: the carrier of Y1 /\ the carrier of Y2 c= the carrier of X1 /\ the carrier of X2 by XBOOLE_1:27;
the carrier of Y1 meets the carrier of Y2 by A1, TSEP_1:def 3;
then the carrier of Y1 /\ the carrier of Y2 <> {} by XBOOLE_0:def 7;
then the carrier of X1 /\ the carrier of X2 <> {} by A2, XBOOLE_1:3, XBOOLE_1:27;
then the carrier of X1 meets the carrier of X2 by XBOOLE_0:def 7;
then X1 meets X2 by TSEP_1:def 3;
then the carrier of Y1 /\ the carrier of Y2 c= the carrier of (X1 meet X2) by A3, TSEP_1:def 5;
then the carrier of (Y1 meet Y2) c= the carrier of (X1 meet X2) by A1, TSEP_1:def 5;
hence Y1 meet Y2 is SubSpace of X1 meet X2 by TSEP_1:4; :: thesis: verum