:: deftheorem Def8 defines with_bottom WAYBEL23:def 8 :
for L being non empty RelStr
for S being Subset of L holds
( S is with_bottom iff Bottom L in S );