let A be Tolerance_Space; :: thesis: for X being Subset of A holds LAp (X `) = (UAp X) `
let X be Subset of A; :: thesis: LAp (X `) = (UAp X) `
LAp (X `) misses UAp X

proof

assume LAp (X `) meets UAp X ; :: thesis: contradiction
then consider x being object such that
A1: ( x in LAp (X `) & x in UAp X ) by XBOOLE_0:3;
( Class ( the InternalRel of A,x) meets X & Class ( the InternalRel of A,x) c= X ` ) by A1, Th8, Th10;
hence contradiction by XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum

end;

hence LAp (X `) c= (UAp X) ` by SUBSET_1:23; :: according to XBOOLE_0:def 10 :: thesis: (UAp X) ` c= LAp (X `)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UAp X) ` or x in LAp (X `) )
assume A2: x in (UAp X) ` ; :: thesis: x in LAp (X `)
then not x in UAp X by XBOOLE_0:def 5;
then Class ( the InternalRel of A,x) misses X by A2;
then Class ( the InternalRel of A,x) c= X ` by SUBSET_1:23;
hence x in LAp (X `) by A2; :: thesis: verum