theorem :: ROUGHS_1:17

for A being Tolerance_Space
for X being Subset of A holds
( X = LAp X iff X = UAp X ) by Th15, Th16;