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