theorem
SubmoduleDirectSum.sup_eq_top_of_finrank_add_eq_and_inf_eq_bot
{F : Type u_1}
{V : Type u_2}
[DivisionRing F]
[AddCommGroup V]
[Module F V]
[FiniteDimensional F V]
(W W' : Submodule F V)
(hdim : Module.finrank F ↥W + Module.finrank F ↥W' = Module.finrank F V)
(hinter : W ⊓ W' = ⊥)
: