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 ) )
proof
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;
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
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;