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 set ; :: 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 set such that
A1: ( y in Class the InternalRel of A,x & y in LAp (UAp X) ) by XBOOLE_0:3;
[y,x] in the InternalRel of A by A1, EQREL_1:27;
then A2: [x,y] in the InternalRel of A by EQREL_1:12;
A3: Class the InternalRel of A,y c= UAp X by A1, Th8;
x in Class the InternalRel of A,y by A2, EQREL_1:27;
hence x in UAp X by A3; :: thesis: verum

end;

thus UAp X c= UAp (LAp (UAp X)) :: thesis: verum

proof

X c= LAp (UAp X)

proof

let x be set ; :: 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 set ; :: 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:27;
then [x,y] in the InternalRel of A by EQREL_1:12;
then x in Class the InternalRel of A,y by EQREL_1:27;
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

end;