let A be Tolerance_Space; :: thesis: UAp ([#] A) = [#] A
LAp ([#] A) c= UAp ([#] A) by Th14;
then [#] A c= UAp ([#] A) by Th20;
hence UAp ([#] A) = [#] A ; :: thesis: verum