let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
let V be finite-dimensional VectSp of GF; :: 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 + W2) <= dim V & (dim V) + ((dim (W1 /\ W2)) - (dim V)) = dim (W1 /\ W2) ) by Th25;
((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th32
.= (dim (W1 + W2)) + ((dim (W1 /\ W2)) - (dim V)) ;
hence dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) by A1, XREAL_1:6; :: thesis: verum