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