let A be Tolerance_Space; :: thesis: UAp ({} A) = {}
assume UAp ({} A) <> {} ; :: thesis: contradiction
then consider x being set such that
A1: x in UAp ({} A) by XBOOLE_0:def 1;
consider y being Element of A such that
A2: ( y = x & Class the InternalRel of A,y meets {} A ) by A1;
thus contradiction by A2, XBOOLE_1:65; :: thesis: verum