take the non void M bounded SimplicialComplex of the set ; :: thesis: ( the non void M bounded SimplicialComplex of the set is M bounded & not the non void M bounded SimplicialComplex of the set is void & the non void M bounded SimplicialComplex of the set is subset-closed & the non void M bounded SimplicialComplex of the set is finite-membered )
thus ( the non void M bounded SimplicialComplex of the set is M bounded & not the non void M bounded SimplicialComplex of the set is void & the non void M bounded SimplicialComplex of the set is subset-closed & the non void M bounded SimplicialComplex of the set is finite-membered ) ; :: thesis: verum