theorem :: RELSET_3:10

succRel omega = { [n,(n + 1)] where n is Nat : verum }