set X = the non empty natural-membered set ;
take the non empty natural-membered set ; :: thesis: ( not the non empty natural-membered set is empty & the non empty natural-membered set is natural-membered )
thus ( not the non empty natural-membered set is empty & the non empty natural-membered set is natural-membered ) ; :: thesis: verum