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 )
set I = the affinely-independent Subset of V;
thus ( not {the affinely-independent Subset of V} is empty & {the affinely-independent Subset of V} is affinely-independent ) ; :: thesis: verum