It is a bit hard to understand from your posting what exactly you are trying to achieve. The property that you state is expressed in TLA+ as the temporal formula
Monotonic == [][x' >= x]_x
This definition of formula Monotonic would appear in a TLA module that contains a declaration
VARIABLE x
Now the question is what algorithm Monotonic is a property of. For example, you could write the specification
CONSTANT N
Init == x = 0
Next == x < N /\ x' = x+1
Spec == Init /\ [][Next]_x
and use TLC to check that
Spec => Monotonic
holds (by entering Monotonic as a property to be checked of specification Spec). TLC will require you to instantiate the parameter N, say by the number 10. This is necessary so that the instance that TLC verifies has a finite state space.
There are many other algorithms that satisfy property Monotonic. In TLA+, there is no formal distinction between specifications and properties of algorithms: both are expressed using temporal formulas. These concepts and many more are explained in the TLA+ documentation that is available on the Web, in particular the TLA+ Hyperbook.
Regards,
Stephan