let R be non empty transitive mediate RelStr ; :: thesis: for X being Subset of R holds UAp X = UAp (UAp X)
let X be Subset of R; :: thesis: UAp X = UAp (UAp X)
A0: UAp X c= UAp (UAp X) by ROUGHS_2:39;
UAp (UAp X) c= UAp X by Th95H;
hence UAp X = UAp (UAp X) by A0, XBOOLE_0:def 10; :: thesis: verum