let A be Tolerance_Space; :: thesis: for X being Subset of A holds X c= UAp X
let X be Subset of A; :: thesis: X c= UAp X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in UAp X )
assume A1: x in X ; :: thesis: x in UAp X
then reconsider x9 = x as Element of A ;
x9 in Class the InternalRel of A,x9 by EQREL_1:28;
then Class the InternalRel of A,x9 meets X by A1, XBOOLE_0:3;
hence x in UAp X ; :: thesis: verum