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

hereby :: thesis: ( UAp X = X implies X is exact )

assume X is exact ; :: thesis: UAp X = X
then BndAp X = {} ;
then A1: UAp X c= LAp X by XBOOLE_1:37;
A2: X c= UAp X by Th13;
LAp X c= X by Th12;
then UAp X c= X by A1;
hence UAp X = X by A2; :: thesis: verum

end;

assume A3: UAp X = X ; :: thesis: X is exact
X c= LAp X

proof

let x be object ; :: 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 object ; :: 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:19;
then [x,y] in the InternalRel of A by EQREL_1:6;
then x in Class ( the InternalRel of A,y) by EQREL_1:19;
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 X is exact ; :: thesis: verum