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 X2 union Y by Th22;
then A2: the carrier of Y c= the carrier of (X2 union Y) by Th4;
Y is SubSpace of X1 union Y by Th22;
then the carrier of Y c= the carrier of (X1 union Y) by Th4;
then the carrier of (X1 union Y) /\ the carrier of (X2 union Y) <> {} by A2, 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 A3: X1 union Y meets X2 union Y ;
A4: 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, Def4
.= ( 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 A3, Def4 ;
hence (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) by Th5; :: thesis: Y union (X1 meet X2) = (Y union X1) meet (Y union X2)
thus Y union (X1 meet X2) = (Y union X1) meet (Y union X2) by A4, Th5; :: thesis: verum