let A be Tolerance_Space; :: thesis: for X being Subset of A holds
( not X is rough iff LAp X = X )
let X be Subset of A; :: thesis: ( not X is rough iff LAp X = X )
A1: LAp X c= UAp X by Th14;

hereby :: thesis: ( LAp X = X implies not X is rough )

assume not X is rough ; :: thesis: LAp X = X
then BndAp X = {} by Def7;
then UAp X c= LAp X by XBOOLE_1:37;
then UAp X = LAp X by A1, XBOOLE_0:def 10;
then A2: X c= LAp X by Th13;
LAp X c= X by Th12;
hence LAp X = X by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume A3: LAp X = X ; :: thesis: not X is rough
UAp X c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp X or y in X )
assume y in UAp X ; :: thesis: y in X
then Class the InternalRel of A,y meets X by Th10;
then consider z being set such that
A4: ( z in Class the InternalRel of A,y & z in LAp X ) by A3, XBOOLE_0:3;
A5: Class the InternalRel of A,z c= X by A4, Th8;
y in Class the InternalRel of A,z by A4, Th7;
hence y in X by A5; :: thesis: verum

end;

then BndAp X = {} by A3, XBOOLE_1:37;
hence not X is rough by Def7; :: thesis: verum