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