theorem Th12: :: WAYBEL_4:12

for L being lower-bounded sup-Semilattice
for x being Element of L
for AR being auxiliary(i) Relation of L holds AR -below x c= downarrow x