theorem Th17: :: MYCIELSK:17

for R being RelStr
for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds
not a <= b