take 0 ; :: thesis: ( 0 is zero & 0 is natural )
thus ( 0 is zero & 0 is natural ) ; :: thesis: verum