take 1 ; :: thesis: 1 is geq_than_1
thus 1 is geq_than_1 by defH; :: thesis: verum