let A be discrete Approximation_Space; :: thesis: for X being Subset of A holds X is exact
let X be Subset of A; :: thesis: X is exact
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 object ; :: 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 object 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:25;
hence x in X by A3, TARSKI:def 1; :: thesis: verum

end;

hence X is exact ; :: thesis: verum