theorem Th11: :: PARTIT_2:11

for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a