:: deftheorem GreatDef defines _greater FUZIMPL3:def 20 :
for x, l being Real holds
( l is x _greater iff l > x );