take 0 ; :: thesis: 0 is zero
thus 0 is zero ; :: thesis: verum