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