let V be RealLinearSpace; :: thesis: for W1, W2, W3 being Subspace of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let W1, W2, W3 be Subspace of V; :: thesis: W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
set V1 = the carrier of W1;
set V2 = the carrier of W2;
set V3 = the carrier of W3;
the carrier of (W1 /\ (W2 /\ W3)) = the carrier of W1 /\ the carrier of (W2 /\ W3) by Def2
.= the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) by Def2
.= ( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 by XBOOLE_1:16
.= the carrier of (W1 /\ W2) /\ the carrier of W3 by Def2 ;
hence W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by Def2; :: thesis: verum