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