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;

( ( 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;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

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

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: verumassume 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;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