theorem Th20: :: UNIFORM3:44

for X being set
for R being Relation of X holds
( rho R is upper & rho R is cap-closed )