let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 holds

X1 meet X2 is SubSpace of X0

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 )

assume A1: X1 meets X2 ; :: thesis: ( not X1 is SubSpace of X0 or not X2 is SubSpace of X0 or X1 meet X2 is SubSpace of X0 )

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

then ( the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 ) by TSEP_1:4;

then A2: the carrier of X1 \/ the carrier of X2 c= the carrier of X0 by XBOOLE_1:8;

the carrier of X1 /\ the carrier of X2 c= the carrier of X1 \/ the carrier of X2 by XBOOLE_1:29;

then the carrier of X1 /\ the carrier of X2 c= the carrier of X0 by A2, XBOOLE_1:1;

then the carrier of (X1 meet X2) c= the carrier of X0 by A1, TSEP_1:def 4;

hence X1 meet X2 is SubSpace of X0 by TSEP_1:4; :: thesis: verum

X1 meet X2 is SubSpace of X0

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 )

assume A1: X1 meets X2 ; :: thesis: ( not X1 is SubSpace of X0 or not X2 is SubSpace of X0 or X1 meet X2 is SubSpace of X0 )

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

then ( the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 ) by TSEP_1:4;

then A2: the carrier of X1 \/ the carrier of X2 c= the carrier of X0 by XBOOLE_1:8;

the carrier of X1 /\ the carrier of X2 c= the carrier of X1 \/ the carrier of X2 by XBOOLE_1:29;

then the carrier of X1 /\ the carrier of X2 c= the carrier of X0 by A2, XBOOLE_1:1;

then the carrier of (X1 meet X2) c= the carrier of X0 by A1, TSEP_1:def 4;

hence X1 meet X2 is SubSpace of X0 by TSEP_1:4; :: thesis: verum