let A be Tolerance_Space; :: thesis: for X being Subset of A holds UAp (X `) = (LAp X) `
let X be Subset of A; :: thesis: UAp (X `) = (LAp X) `
((UAp (X `)) `) ` = (LAp ((X `) `)) ` by Th28;
hence UAp (X `) = (LAp X) ` ; :: thesis: verum