:: deftheorem Def1 defines _greater NAT_6:def 1 :
for n, x being natural number holds
( x is n _greater iff x > n );