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

( ( ( X1 misses X0 or X0 misses X1 ) & ( X2 meets X0 or X0 meets X2 ) implies ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) ) & ( ( X1 meets X0 or X0 meets X1 ) & ( X2 misses X0 or X0 misses X2 ) implies ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) ) )

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

reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;

thus ( ( X1 misses X0 or X0 misses X1 ) & ( X2 meets X0 or X0 meets X2 ) implies ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) ) :: thesis: ( ( X1 meets X0 or X0 meets X1 ) & ( X2 misses X0 or X0 misses X2 ) implies ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) )

( ( ( X1 misses X0 or X0 misses X1 ) & ( X2 meets X0 or X0 meets X2 ) implies ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) ) & ( ( X1 meets X0 or X0 meets X1 ) & ( X2 misses X0 or X0 misses X2 ) implies ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) ) )

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

reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;

thus ( ( X1 misses X0 or X0 misses X1 ) & ( X2 meets X0 or X0 meets X2 ) implies ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) ) :: thesis: ( ( X1 meets X0 or X0 meets X1 ) & ( X2 misses X0 or X0 misses X2 ) implies ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) )

proof

thus
( ( X1 meets X0 or X0 meets X1 ) & ( X2 misses X0 or X0 misses X2 ) implies ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) )
:: thesis: verum
assume that

A1: ( X1 misses X0 or X0 misses X1 ) and

A2: ( X2 meets X0 or X0 meets X2 ) ; :: thesis: ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 )

A3: A1 misses A0 by A1, TSEP_1:def 3;

X2 is SubSpace of X1 union X2 by TSEP_1:22;

then A4: X1 union X2 meets X0 by A2, Th18;

then A5: the carrier of (X0 meet (X1 union X2)) = A0 /\ the carrier of (X1 union X2) by TSEP_1:def 4

.= A0 /\ (A1 \/ A2) by TSEP_1:def 2

.= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23

.= the carrier of (X0 meet X2) by A2, TSEP_1:def 4, A3 ;

the carrier of ((X1 union X2) meet X0) = the carrier of (X1 union X2) /\ A0 by A4, TSEP_1:def 4

.= (A1 \/ A2) /\ A0 by TSEP_1:def 2

.= (A1 /\ A0) \/ (A2 /\ A0) by XBOOLE_1:23

.= the carrier of (X2 meet X0) by A2, TSEP_1:def 4, A3 ;

hence ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) by A5, TSEP_1:5; :: thesis: verum

end;A1: ( X1 misses X0 or X0 misses X1 ) and

A2: ( X2 meets X0 or X0 meets X2 ) ; :: thesis: ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 )

A3: A1 misses A0 by A1, TSEP_1:def 3;

X2 is SubSpace of X1 union X2 by TSEP_1:22;

then A4: X1 union X2 meets X0 by A2, Th18;

then A5: the carrier of (X0 meet (X1 union X2)) = A0 /\ the carrier of (X1 union X2) by TSEP_1:def 4

.= A0 /\ (A1 \/ A2) by TSEP_1:def 2

.= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23

.= the carrier of (X0 meet X2) by A2, TSEP_1:def 4, A3 ;

the carrier of ((X1 union X2) meet X0) = the carrier of (X1 union X2) /\ A0 by A4, TSEP_1:def 4

.= (A1 \/ A2) /\ A0 by TSEP_1:def 2

.= (A1 /\ A0) \/ (A2 /\ A0) by XBOOLE_1:23

.= the carrier of (X2 meet X0) by A2, TSEP_1:def 4, A3 ;

hence ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) by A5, TSEP_1:5; :: thesis: verum

proof

assume that

A6: ( X1 meets X0 or X0 meets X1 ) and

A7: ( X2 misses X0 or X0 misses X2 ) ; :: thesis: ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 )

A8: A2 misses A0 by A7, TSEP_1:def 3;

X1 is SubSpace of X1 union X2 by TSEP_1:22;

then A9: X1 union X2 meets X0 by A6, Th18;

then A10: the carrier of (X0 meet (X1 union X2)) = A0 /\ the carrier of (X1 union X2) by TSEP_1:def 4

.= A0 /\ (A1 \/ A2) by TSEP_1:def 2

.= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23

.= the carrier of (X0 meet X1) by A6, TSEP_1:def 4, A8 ;

the carrier of ((X1 union X2) meet X0) = the carrier of (X1 union X2) /\ A0 by A9, TSEP_1:def 4

.= (A1 \/ A2) /\ A0 by TSEP_1:def 2

.= (A1 /\ A0) \/ {} by A8, XBOOLE_1:23

.= the carrier of (X1 meet X0) by A6, TSEP_1:def 4 ;

hence ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) by A10, TSEP_1:5; :: thesis: verum

end;A6: ( X1 meets X0 or X0 meets X1 ) and

A7: ( X2 misses X0 or X0 misses X2 ) ; :: thesis: ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 )

A8: A2 misses A0 by A7, TSEP_1:def 3;

X1 is SubSpace of X1 union X2 by TSEP_1:22;

then A9: X1 union X2 meets X0 by A6, Th18;

then A10: the carrier of (X0 meet (X1 union X2)) = A0 /\ the carrier of (X1 union X2) by TSEP_1:def 4

.= A0 /\ (A1 \/ A2) by TSEP_1:def 2

.= (A0 /\ A1) \/ (A0 /\ A2) by XBOOLE_1:23

.= the carrier of (X0 meet X1) by A6, TSEP_1:def 4, A8 ;

the carrier of ((X1 union X2) meet X0) = the carrier of (X1 union X2) /\ A0 by A9, TSEP_1:def 4

.= (A1 \/ A2) /\ A0 by TSEP_1:def 2

.= (A1 /\ A0) \/ {} by A8, XBOOLE_1:23

.= the carrier of (X1 meet X0) by A6, TSEP_1:def 4 ;

hence ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) by A10, TSEP_1:5; :: thesis: verum