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

end;

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

end;