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 object ; :: 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:20;
then Class ( the InternalRel of A,x9) meets X by A1, XBOOLE_0:3;
hence x in UAp X ; :: thesis: verum