theorem Th9: :: ROUGHS_2:9

for R being non empty RelStr
for X being Subset of R holds Lap X = LAp X