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