theorem Th17: :: WAYBEL_4:17

for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) Relation of L
for x, y being Element of L st x <= y holds
AR -below x c= AR -below y