let X be non empty TopSpace; :: thesis: for X1, X2, Y1, Y2 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 X1, X2, Y1, Y2 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;
the carrier of Y1 meets the carrier of Y2 by A1, TSEP_1:def 3;
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 ;
then A3: X1 meets X2 by TSEP_1:def 3;
the carrier of Y1 /\ the carrier of Y2 c= the carrier of X1 /\ the carrier of X2 by A2, XBOOLE_1:27;
then the carrier of Y1 /\ the carrier of Y2 c= the carrier of (X1 meet X2) by A3, TSEP_1:def 4;
then the carrier of (Y1 meet Y2) c= the carrier of (X1 meet X2) by A1, TSEP_1:def 4;
hence Y1 meet Y2 is SubSpace of X1 meet X2 by TSEP_1:4; :: thesis: verum