theorem Th4: :: MIDSP_3:4

for j, l being Nat holds
( l <= j or l = j + 1 or j + 2 <= l )