let A be Tolerance_Space; :: thesis: for X being Subset of holds
( X = LAp X iff X = UAp X )
let X be Subset of ; :: thesis: ( X = LAp X iff X = UAp X )
( X = LAp X iff not X is rough ) by Th15;
hence ( X = LAp X iff X = UAp X ) by Th16; :: thesis: verum