set v = the Element of V;
take Complex_of {{ the Element of V}} ; :: thesis: ( Complex_of {{ the Element of V}} is with_non-empty_element & 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 ( Complex_of {{ the Element of V}} is with_non-empty_element & 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 ) ; :: thesis: verum