let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2 ) & ( X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0 ) )
let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( ( X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2 ) & ( X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0 ) ) )
reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: X1 meets X2 ; :: thesis: ( ( X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2 ) & ( X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0 ) )
then A2: the carrier of (X1 meet X2) = A1 /\ A2 by TSEP_1:def 4;

A3: now :: thesis: ( X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0 )

assume A4: X2 is SubSpace of X0 ; :: thesis: X1 meet X2 is SubSpace of X1 meet X0
then A5: A1 /\ A2 c= A1 /\ A0 by XBOOLE_1:26, TSEP_1:4;
X1 meets X0 by A1, A4, Th18;
then the carrier of (X1 meet X0) = A1 /\ A0 by TSEP_1:def 4;
hence X1 meet X2 is SubSpace of X1 meet X0 by A2, A5, TSEP_1:4; :: thesis: verum

end;

now :: thesis: ( X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2 )

assume A6: X1 is SubSpace of X0 ; :: thesis: X1 meet X2 is SubSpace of X0 meet X2
then A1 c= A0 by TSEP_1:4;
then A7: A1 /\ A2 c= A0 /\ A2 by XBOOLE_1:26;
X0 meets X2 by A1, A6, Th18;
then the carrier of (X0 meet X2) = A0 /\ A2 by TSEP_1:def 4;
hence X1 meet X2 is SubSpace of X0 meet X2 by A2, A7, TSEP_1:4; :: thesis: verum

end;

hence ( ( X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2 ) & ( X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0 ) ) by A3; :: thesis: verum