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