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