take 1 / 1 ; :: thesis: 1 / 1 is positive
thus 1 / 1 is positive ; :: thesis: verum