:: deftheorem defines Lower DILWORTH:def 7 :
for R being RelStr
for X being Subset of R holds Lower X = X \/ (downarrow X);