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

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