set v = the Element of V;
take C = Complex_of {{the Element of V}}; ( not C is empty-membered & C is finite-vertices & C is affinely-independent & C is simplex-join-closed & C is total )
thus
( not C is empty-membered & C is finite-vertices & C is affinely-independent & C is simplex-join-closed & C is total )
by SIMPLEX0:def 7; verum