theorem NF600: :: BINPACK1:4

for a, b being Nat
for s being set holds
( not (Seg a) \/ {s} = Seg b or a = b or a + 1 = b )