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