let X be non empty TopSpace; :: thesis: for X1, X2, X3 being non empty SubSpace of X holds
( ( X1 meets X2 implies X1 meet X2 = X2 meet X1 ) & ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) ) )
let X1, X2, X3 be non empty SubSpace of X; :: thesis: ( ( X1 meets X2 implies X1 meet X2 = X2 meet X1 ) & ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) ) )
thus ( X1 meets X2 implies X1 meet X2 = X2 meet X1 ) :: thesis: ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) )

proof

assume A1: X1 meets X2 ; :: thesis: X1 meet X2 = X2 meet X1
then the carrier of (X1 meet X2) = the carrier of X2 /\ the carrier of X1 by Def4
.= the carrier of (X2 meet X1) by A1, Def4 ;
hence X1 meet X2 = X2 meet X1 by Th5; :: thesis: verum

end;

now :: thesis: ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) )

A2: now :: thesis: ( X1 meets X2 & X1 meet X2 meets X3 implies ( X1 meets X2 & X1 meet X2 meets X3 & X2 meets X3 & X1 meets X2 meet X3 ) )

assume that
A3: X1 meets X2 and
A4: X1 meet X2 meets X3 ; :: thesis: ( X1 meets X2 & X1 meet X2 meets X3 & X2 meets X3 & X1 meets X2 meet X3 )
the carrier of (X1 meet X2) meets the carrier of X3 by A4;
then the carrier of (X1 meet X2) /\ the carrier of X3 <> {} by XBOOLE_0:def 7;
then ( the carrier of X1 /\ the carrier of X2) /\ the carrier of X3 <> {} by A3, Def4;
then A5: the carrier of X1 /\ ( the carrier of X2 /\ the carrier of X3) <> {} by XBOOLE_1:16;
then the carrier of X2 /\ the carrier of X3 <> {} ;
then A6: the carrier of X2 meets the carrier of X3 by XBOOLE_0:def 7;
then X2 meets X3 ;
then the carrier of X1 /\ the carrier of (X2 meet X3) <> {} by A5, Def4;
then the carrier of X1 meets the carrier of (X2 meet X3) by XBOOLE_0:def 7;
hence ( X1 meets X2 & X1 meet X2 meets X3 & X2 meets X3 & X1 meets X2 meet X3 ) by A3, A4, A6; :: thesis: verum

end;

assume A7: ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) ; :: thesis: (X1 meet X2) meet X3 = X1 meet (X2 meet X3)

A8: now :: thesis: ( X2 meets X3 & X1 meets X2 meet X3 implies ( X1 meets X2 & X1 meet X2 meets X3 & X2 meets X3 & X1 meets X2 meet X3 ) )

assume that
A9: X2 meets X3 and
A10: X1 meets X2 meet X3 ; :: thesis: ( X1 meets X2 & X1 meet X2 meets X3 & X2 meets X3 & X1 meets X2 meet X3 )
the carrier of X1 meets the carrier of (X2 meet X3) by A10;
then the carrier of X1 /\ the carrier of (X2 meet X3) <> {} by XBOOLE_0:def 7;
then the carrier of X1 /\ ( the carrier of X2 /\ the carrier of X3) <> {} by A9, Def4;
then A11: ( the carrier of X1 /\ the carrier of X2) /\ the carrier of X3 <> {} by XBOOLE_1:16;
then the carrier of X1 /\ the carrier of X2 <> {} ;
then A12: the carrier of X1 meets the carrier of X2 by XBOOLE_0:def 7;
then X1 meets X2 ;
then the carrier of (X1 meet X2) /\ the carrier of X3 <> {} by A11, Def4;
then the carrier of (X1 meet X2) meets the carrier of X3 by XBOOLE_0:def 7;
hence ( X1 meets X2 & X1 meet X2 meets X3 & X2 meets X3 & X1 meets X2 meet X3 ) by A9, A10, A12; :: thesis: verum

end;

then the carrier of ((X1 meet X2) meet X3) = the carrier of (X1 meet X2) /\ the carrier of X3 by A7, Def4
.= ( the carrier of X1 /\ the carrier of X2) /\ the carrier of X3 by A7, A8, Def4
.= the carrier of X1 /\ ( the carrier of X2 /\ the carrier of X3) by XBOOLE_1:16
.= the carrier of X1 /\ the carrier of (X2 meet X3) by A7, A2, Def4
.= the carrier of (X1 meet (X2 meet X3)) by A7, A2, Def4 ;
hence (X1 meet X2) meet X3 = X1 meet (X2 meet X3) by Th5; :: thesis: verum

end;

hence ( ( ( X1 meets X2 & X1 meet X2 meets X3 ) or ( X2 meets X3 & X1 meets X2 meet X3 ) ) implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3) ) ; :: thesis: verum