take {} V ; :: thesis: {} V is linearly-independent
thus {} V is linearly-independent ; :: thesis: verum