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