:: deftheorem defines upper-bounded YELLOW21:def 9 :
for R being Relation holds
( R is upper-bounded iff ex x being set st
for y being set st y in field R holds
[y,x] in R );