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

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

end;

now

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

A3: now

assume A4: ( X1 meets X2 & X1 meet X2 meets X3 ) ; :: thesis:
then the carrier of (X1 meet X2) meets the carrier of X3 by Def3;
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 A4, Def5;
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 by Def3;
then the carrier of X1 /\ the carrier of (X2 meet X3) <> {} by A5, Def5;
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 A4, A6, Def3; :: thesis:

end;

A7: now

assume A8: ( X2 meets X3 & X1 meets X2 meet X3 ) ; :: thesis:
then the carrier of X1 meets the carrier of (X2 meet X3) by Def3;
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 A8, Def5;
then A9: (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 A10: the carrier of X1 meets the carrier of X2 by XBOOLE_0:def 7;
then X1 meets X2 by Def3;
then the carrier of (X1 meet X2) /\ the carrier of X3 <> {} by A9, Def5;
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 A8, A10, Def3; :: thesis:

end;

then the carrier of ((X1 meet X2) meet X3) = the carrier of (X1 meet X2) /\ the carrier of X3 by A2, Def5
.= (the carrier of X1 /\ the carrier of X2) /\ the carrier of X3 by A2, A7, Def5
.= 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 A2, A3, Def5
.= the carrier of (X1 meet (X2 meet X3)) by A2, A3, Def5 ;
hence (X1 meet X2) meet X3 = X1 meet (X2 meet X3) by Th5; :: thesis:

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: