theorem Th60: :: YELLOW_0:60

for L being RelStr
for S being full SubRelStr of L
for a, b being Element of L
for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds
x <= y