let A be Tolerance_Space; :: thesis: LAp ([#] A) = [#] A
thus LAp ([#] A) c= [#] A ; :: according to XBOOLE_0:def 10 :: thesis: [#] A c= LAp ([#] A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] A or x in LAp ([#] A) )
A1: Class ( the InternalRel of A,x) c= [#] A ;
assume x in [#] A ; :: thesis: x in LAp ([#] A)
hence x in LAp ([#] A) by A1; :: thesis: verum