:: deftheorem Def9 defines AuxBottom WAYBEL_4:def 9 :
for L being non empty RelStr
for b₂ being Relation of L holds
( b₂ = AuxBottom L iff for x, y being Element of L holds
( [x,y] in b₂ iff x = Bottom L ) );