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 set ; :: 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:28;
hence x in X by A1; :: thesis: verum