let A be Tolerance_Space; :: thesis: for X being Subset of holds LAp X c= UAp X
let X be Subset of ; :: thesis: LAp X c= UAp X
( LAp X c= X & X c= UAp X ) by Th12, Th13;
hence LAp X c= UAp X by XBOOLE_1:1; :: thesis: verum