let A be Tolerance_Space; :: thesis: for X being Subset of A holds LAp X c= X
let X be Subset of A; :: thesis: LAp X c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LAp X or x in X )
assume x in LAp X ; :: thesis: x in X
then consider y being Element of A such that
A1: ( y = x & Class ( the InternalRel of A,y) c= X ) ;
y in Class ( the InternalRel of A,y) by EQREL_1:20;
hence x in X by A1; :: thesis: verum