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 set ; :: 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 X & Class the InternalRel of A,x meets Y ) by Th10, XBOOLE_1:74;
then ( x in UAp X & x in UAp Y ) by A1;
hence x in (UAp X) /\ (UAp Y) by XBOOLE_0:def 4; :: thesis: verum