:: deftheorem defines dense WAYBEL12:def 4 :
for L being non empty RelStr
for u being Element of L holds
( u is dense iff for v being Element of L st v <> Bottom L holds
u "/\" v <> Bottom L );