take 2 ; :: thesis: 2 is 1 _greater
thus 2 is 1 _greater ; :: thesis: verum