let X be non empty TopSpace; :: thesis: for X1, X2, Y being non empty SubSpace of X st X1 meets X2 holds
( (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) & Y union (X1 meet X2) = (Y union X1) meet (Y union X2) )
let X1, X2, Y be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) & Y union (X1 meet X2) = (Y union X1) meet (Y union X2) ) )
assume A1: X1 meets X2 ; :: thesis: ( (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) & Y union (X1 meet X2) = (Y union X1) meet (Y union X2) )
( Y is SubSpace of X1 union Y & Y is SubSpace of X2 union Y ) by Th22;
then ( the carrier of Y c= the carrier of (X1 union Y) & the carrier of Y c= the carrier of (X2 union Y) ) by Th4;
then the carrier of (X1 union Y) /\ the carrier of (X2 union Y) <> {} by XBOOLE_1:3, XBOOLE_1:19;
then the carrier of (X1 union Y) meets the carrier of (X2 union Y) by XBOOLE_0:def 7;
then A2: X1 union Y meets X2 union Y by Def3;
thus (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) :: thesis: Y union (X1 meet X2) = (Y union X1) meet (Y union X2)

proof

the carrier of ((X1 meet X2) union Y) = the carrier of (X1 meet X2) \/ the carrier of Y by Def2
.= (the carrier of X1 /\ the carrier of X2) \/ the carrier of Y by A1, Def5
.= (the carrier of X1 \/ the carrier of Y) /\ (the carrier of X2 \/ the carrier of Y) by XBOOLE_1:24
.= the carrier of (X1 union Y) /\ (the carrier of X2 \/ the carrier of Y) by Def2
.= the carrier of (X1 union Y) /\ the carrier of (X2 union Y) by Def2
.= the carrier of ((X1 union Y) meet (X2 union Y)) by A2, Def5 ;
hence (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) by Th5; :: thesis: verum

end;

hence Y union (X1 meet X2) = (Y union X1) meet (Y union X2) ; :: thesis: verum