take { the Element of V} ; :: thesis: ( not { the Element of V} is empty & { the Element of V} is trivial & { the Element of V} is affinely-independent )
thus ( not { the Element of V} is empty & { the Element of V} is trivial & { the Element of V} is affinely-independent ) ; :: thesis: verum