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

proof

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

end;

hence LAp (UAp (LAp X)) c= LAp X by Th24; :: according to XBOOLE_0:def 10 :: thesis: LAp X c= LAp (UAp (LAp X))
thus LAp X c= LAp (UAp (LAp X)) :: thesis: verum

proof

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

end;

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

end;