take 0 ; :: thesis: 0 is - 1 _greater
thus 0 is - 1 _greater ; :: thesis: verum