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
A1: LAp X c= X by Th12;
X c= UAp X by Th13;
hence LAp X c= UAp X by A1, XBOOLE_1:1; :: thesis: verum