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