take { the Element of V} ; :: thesis: ( { the Element of V} is 1 -element & { the Element of V} is affinely-independent )
thus ( { the Element of V} is 1 -element & { the Element of V} is affinely-independent ) ; :: thesis: verum