let V be finite-dimensional RealUnitarySpace; :: 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 Th8;

((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th15

.= (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

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 Th8;

((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th15

.= (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