take {0} ; :: thesis: ( not {0} is empty & {0} is finite & {0} is natural-membered )
thus ( not {0} is empty & {0} is finite & {0} is natural-membered ) ; :: thesis: verum