take StructVectSp K ; :: thesis: not StructVectSp K is trivial
thus not StructVectSp K is trivial ; :: thesis: verum