for m, n being Nat holds
( Domin_0 (n,m) is empty iff 2 * m > n )