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

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

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

end;

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

proof

let y be object ; :: 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 object such that
A4: ( z in Class ( the InternalRel of A,y) & z in LAp X ) by A3, XBOOLE_0:3;
( Class ( the InternalRel of A,z) c= X & y in Class ( the InternalRel of A,z) ) by A4, Th7, Th8;
hence y in X ; :: thesis: verum

end;

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