let A be discrete Approximation_Space; :: thesis: for X being Subset of A holds not X is rough
let X be Subset of A; :: thesis: not X is rough
A1: the InternalRel of A = id the carrier of A by ORDERS_3:def 1;
X = UAp X

proof

thus X c= UAp X by Th13; :: according to XBOOLE_0:def 10 :: thesis: UAp X c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp X or x in X )
assume A2: x in UAp X ; :: thesis: x in X
then Class the InternalRel of A,x meets X by Th10;
then A3: ex y being set st
( y in Class the InternalRel of A,x & y in X ) by XBOOLE_0:3;
Class the InternalRel of A,x = {x} by A1, A2, EQREL_1:33;
hence x in X by A3, TARSKI:def 1; :: thesis: verum

end;

hence not X is rough ; :: thesis: verum