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