let X be non empty TopSpace; :: thesis: for X1, X2, X3 being non empty SubSpace of X holds (X1 union X2) union X3 = X1 union (X2 union X3)
let X1, X2, X3 be non empty SubSpace of X; :: thesis: (X1 union X2) union X3 = X1 union (X2 union X3)
the carrier of ((X1 union X2) union X3) = the carrier of (X1 union X2) \/ the carrier of X3 by Def2
.= ( the carrier of X1 \/ the carrier of X2) \/ the carrier of X3 by Def2
.= the carrier of X1 \/ ( the carrier of X2 \/ the carrier of X3) by XBOOLE_1:4
.= the carrier of X1 \/ the carrier of (X2 union X3) by Def2
.= the carrier of (X1 union (X2 union X3)) by Def2 ;
hence (X1 union X2) union X3 = X1 union (X2 union X3) by Th5; :: thesis: verum