:: deftheorem Def1 defines geq_than_1 LPSPACE2:def 1 :
for r being Real holds
( r is geq_than_1 iff 1 <= r );