let X be non empty TopSpace; 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; ( 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
; ( 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 )
; 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; verum