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