take T = the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set ; :: thesis: ( not T is empty & not T is with_non-empty_elements & not T is empty-membered & T is finite-vertices & T is subset-closed & T is strict )
thus ( not T is empty & not T is with_non-empty_elements & not T is empty-membered & T is finite-vertices & T is subset-closed & T is strict ) ; :: thesis: verum