take the natural non zero object ; :: thesis: ( not the natural non zero object is zero & the natural non zero object is ext-natural )
thus ( not the natural non zero object is zero & the natural non zero object is ext-natural ) ; :: thesis: verum