theorem Th18: :: MYCIELSK:18

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 & x in the carrier of R & not a <= b holds
x <= y