let S be Subset of V; :: thesis: ( S is empty implies S is Affine )
assume S is empty ; :: thesis: S is Affine
then for x, y being VECTOR of V
for z being Complex st z is Real & x in S & y in S holds
((1r - z) * x) + (z * y) in S ;
hence S is Affine by Def20; :: thesis: verum