:: deftheorem Def12 defines -below WAYBEL_4:def 12 :
for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L
for b₃ being Function of L,(InclPoset (Ids L)) holds
( b₃ = AR -below iff for x being Element of L holds b₃ . x = AR -below x );