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

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

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in LAp X )
assume A4: x in X ; :: thesis: x in LAp X
Class the InternalRel of A,x c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Class the InternalRel of A,x or y in X )
assume A5: y in Class the InternalRel of A,x ; :: thesis: y in X
then [y,x] in the InternalRel of A by EQREL_1:27;
then [x,y] in the InternalRel of A by EQREL_1:12;
then x in Class the InternalRel of A,y by EQREL_1:27;
then Class the InternalRel of A,y meets X by A4, XBOOLE_0:3;
hence y in X by A3, A5; :: thesis: verum

end;

hence x in LAp X by A4; :: thesis: verum

end;

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