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

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