theorem :: BAGORD_2:6

for x, y being Nat holds
( not x + y > 0 or x > 0 or y > 0 ) ;