let A be Tolerance_Space; :: thesis: for X being Subset of A holds UAp (LAp (UAp X)) = UAp X
let X be Subset of A; :: thesis: UAp (LAp (UAp X)) = UAp X
thus UAp (LAp (UAp X)) c= UAp X :: according to XBOOLE_0:def 10 :: thesis: UAp X c= UAp (LAp (UAp X))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp (LAp (UAp X)) or x in UAp X )
assume x in UAp (LAp (UAp X)) ; :: thesis: x in UAp X
then Class ( the InternalRel of A,x) meets LAp (UAp X) by Th10;
then consider y being object such that
A1: y in Class ( the InternalRel of A,x) and
A2: y in LAp (UAp X) by XBOOLE_0:3;
[y,x] in the InternalRel of A by A1, EQREL_1:19;
then [x,y] in the InternalRel of A by EQREL_1:6;
then A3: x in Class ( the InternalRel of A,y) by EQREL_1:19;
Class ( the InternalRel of A,y) c= UAp X by A2, Th8;
hence x in UAp X by A3; :: thesis: verum

end;

X c= LAp (UAp X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in LAp (UAp X) )
assume A4: x in X ; :: thesis: x in LAp (UAp X)
Class ( the InternalRel of A,x) c= UAp X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Class ( the InternalRel of A,x) or y in UAp X )
assume A5: y in Class ( the InternalRel of A,x) ; :: thesis: y in UAp 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 UAp X by A5; :: thesis: verum

end;

hence x in LAp (UAp X) by A4; :: thesis: verum

end;

hence UAp X c= UAp (LAp (UAp X)) by Th25; :: thesis: verum