let V be finite-dimensional RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
let W1, W2 be Subspace of V; :: thesis: dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
A1: ((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th36
.= (dim (W1 + W2)) + ((dim (W1 /\ W2)) - (dim V)) ;
A2: dim (W1 + W2) <= dim V by Th29;
(dim V) + ((dim (W1 /\ W2)) - (dim V)) = dim (W1 /\ W2) ;
hence dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) by A1, A2, XREAL_1:8; :: thesis: verum