let X be non empty TopSpace; :: thesis:
let X0, X1, X2 be non empty SubSpace of X; :: thesis:
assume A1: X1 meets X2 ; :: thesis:

A2: now :: thesis:

X1 meet X2 is SubSpace of X2 by A1, TSEP_1:27;
then A3: X1 meet X2 meets X2 by Th17;
assume A4: X2 is SubSpace of X0 ; :: thesis:
then X1 meet X2 is SubSpace of X1 meet X0 by A1, Th27;
hence A5: X1 meet X0 meets X2 by A3, Th18; :: thesis:
X1 meets X0 by A1, A4, Th18;
hence X0 meet X1 meets X2 by A5, TSEP_1:26; :: thesis:

end;

X1 meet X2 is SubSpace of X1 by A1, TSEP_1:27;
then A6: X1 meet X2 meets X1 by Th17;
assume A7: X1 is SubSpace of X0 ; :: thesis:
then X1 meet X2 is SubSpace of X0 meet X2 by A1, Th27;
hence A8: X0 meet X2 meets X1 by A6, Th18; :: thesis:
X0 meets X2 by A1, A7, Th18;
hence X2 meet X0 meets X1 by A8, TSEP_1:26; :: thesis:

end;

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