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 ) by REALSET1:def 4; :: thesis: verum