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