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