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

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( ( 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 ) ) ) )

assume A1: X1 meets X2 ; :: thesis: ( ( 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 ) ) )

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

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( ( 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 ) ) ) )

assume A1: X1 meets X2 ; :: thesis: ( ( 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 ) ) )

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

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: ( X1 meet X0 meets X2 & X0 meet X1 meets X2 )

then X1 meet X2 is SubSpace of X1 meet X0 by A1, Th27;

hence A5: X1 meet X0 meets X2 by A3, Th18; :: thesis: X0 meet X1 meets X2

X1 meets X0 by A1, A4, Th18;

hence X0 meet X1 meets X2 by A5, TSEP_1:26; :: thesis: verum

end;then A3: X1 meet X2 meets X2 by Th17;

assume A4: X2 is SubSpace of X0 ; :: thesis: ( X1 meet X0 meets X2 & X0 meet X1 meets X2 )

then X1 meet X2 is SubSpace of X1 meet X0 by A1, Th27;

hence A5: X1 meet X0 meets X2 by A3, Th18; :: thesis: X0 meet X1 meets X2

X1 meets X0 by A1, A4, Th18;

hence X0 meet X1 meets X2 by A5, TSEP_1:26; :: thesis: verum

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

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: verum
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: ( X0 meet X2 meets X1 & X2 meet X0 meets X1 )

then X1 meet X2 is SubSpace of X0 meet X2 by A1, Th27;

hence A8: X0 meet X2 meets X1 by A6, Th18; :: thesis: X2 meet X0 meets X1

X0 meets X2 by A1, A7, Th18;

hence X2 meet X0 meets X1 by A8, TSEP_1:26; :: thesis: verum

end;then A6: X1 meet X2 meets X1 by Th17;

assume A7: X1 is SubSpace of X0 ; :: thesis: ( X0 meet X2 meets X1 & X2 meet X0 meets X1 )

then X1 meet X2 is SubSpace of X0 meet X2 by A1, Th27;

hence A8: X0 meet X2 meets X1 by A6, Th18; :: thesis: X2 meet X0 meets X1

X0 meets X2 by A1, A7, Th18;

hence X2 meet X0 meets X1 by A8, TSEP_1:26; :: thesis: verum