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