:: deftheorem defines Upper DILWORTH:def 8 :
for R being RelStr
for X being Subset of R holds Upper X = X \/ (uparrow X);