theorem Conv: :: ROUGHS_3:29

for R being non empty RelStr st ( for X being Subset of R holds UAp ((UAp X) `) c= (UAp X) ` ) holds
for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)