let A be Tolerance_Space; :: thesis: for X, Y being Subset of A st X c= Y holds
UAp X c= UAp Y
let X, Y be Subset of A; :: thesis: ( X c= Y implies UAp X c= UAp Y )
assume A1: X c= Y ; :: thesis: UAp X c= UAp Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp X or x in UAp Y )
assume A2: x in UAp X ; :: thesis: x in UAp Y
then Class ( the InternalRel of A,x) meets X by Th10;
then Class ( the InternalRel of A,x) meets Y by A1, XBOOLE_1:63;
hence x in UAp Y by A2; :: thesis: verum