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

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