:: deftheorem Def5 defines dense WAYBEL12:def 5 :
for L being non empty RelStr
for D being Subset of L holds
( D is dense iff for d being Element of L st d in D holds
d is dense );