:: deftheorem Def8 defines Aux WAYBEL_4:def 8 :
for L being lower-bounded sup-Semilattice
for b₂ being set holds
( b₂ = Aux L iff for a being set holds
( a in b₂ iff a is auxiliary Relation of L ) );