take [#] V ; :: thesis: ( not [#] V is empty & [#] V is Affine )
thus ( not [#] V is empty & [#] V is Affine ) by Th22; :: thesis: verum