let R be non empty RelStr ; :: thesis: for X, Y being Subset of R holds UAp (X /\ Y) c= (UAp X) /\ (UAp Y)
let X, Y be Subset of R; :: 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 reconsider xx = x as Element of R ;
Class ( the InternalRel of R,x) meets Y by A1, ROUGHS_2:7, XBOOLE_1:74;
then xx in { x where x is Element of R : Class ( the InternalRel of R,x) meets Y } ;
then A2: x in UAp Y by ROUGHS_1:def 5;
Class ( the InternalRel of R,x) meets X by A1, ROUGHS_2:7, XBOOLE_1:74;
then xx in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } ;
then x in UAp X by ROUGHS_1:def 5;
hence x in (UAp X) /\ (UAp Y) by A2, XBOOLE_0:def 4; :: thesis: verum