let X be non empty TopSpace; :: thesis: for X1, X2, Y being non empty SubSpace of X st X1 meets Y & Y meets X2 holds
( (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) & Y meet (X1 union X2) = (Y meet X1) union (Y meet X2) )
let X1, X2, Y be non empty SubSpace of X; :: thesis: ( X1 meets Y & Y meets X2 implies ( (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) & Y meet (X1 union X2) = (Y meet X1) union (Y meet X2) ) )
assume that
A1: X1 meets Y and
A2: Y meets X2 ; :: thesis: ( (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) & Y meet (X1 union X2) = (Y meet X1) union (Y meet X2) )
X1 is SubSpace of X1 union X2 by Th22;
then A3: the carrier of X1 c= the carrier of (X1 union X2) by Th4;
the carrier of X1 meets the carrier of Y by A1;
then the carrier of X1 /\ the carrier of Y <> {} by XBOOLE_0:def 7;
then the carrier of (X1 union X2) /\ the carrier of Y <> {} by A3, XBOOLE_1:3, XBOOLE_1:26;
then the carrier of (X1 union X2) meets the carrier of Y by XBOOLE_0:def 7;
then A4: X1 union X2 meets Y ;
then the carrier of ((X1 union X2) meet Y) = the carrier of (X1 union X2) /\ the carrier of Y by Def4
.= ( the carrier of X1 \/ the carrier of X2) /\ the carrier of Y by Def2
.= ( the carrier of X1 /\ the carrier of Y) \/ ( the carrier of X2 /\ the carrier of Y) by XBOOLE_1:23
.= the carrier of (X1 meet Y) \/ ( the carrier of X2 /\ the carrier of Y) by A1, Def4
.= the carrier of (X1 meet Y) \/ the carrier of (X2 meet Y) by A2, Def4
.= the carrier of ((X1 meet Y) union (X2 meet Y)) by Def2 ;
hence (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) by Th5; :: thesis: Y meet (X1 union X2) = (Y meet X1) union (Y meet X2)
hence Y meet (X1 union X2) = (X1 meet Y) union (X2 meet Y) by A4, Th26
.= (Y meet X1) union (X2 meet Y) by A1, Th26
.= (Y meet X1) union (Y meet X2) by A2, Th26 ;
:: thesis: verum