theorem Th17: :: ROUGHS_2:17

for R being non empty serial RelStr
for X being Subset of R holds LAp X c= UAp X