let A be Tolerance_Space; :: thesis: for X being Subset of A holds
( X = LAp X iff X = UAp X )
let X be Subset of A; :: 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