for i, j being Nat st i <= j holds
(0* j) | i = 0* i