let R be non empty RelStr ; :: thesis: for X, Y being Subset of R holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)
let X, Y be Subset of R; :: thesis: LAp (X /\ Y) = (LAp X) /\ (LAp Y)
{ x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } = { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }

proof

thus { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } c= { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } c= { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } or y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } )
assume y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } ; :: thesis: y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
then consider z being Element of R such that
A1: ( z = y & Class ( the InternalRel of R,z) c= X /\ Y ) ;
( X /\ Y c= X & X /\ Y c= Y ) by XBOOLE_1:17;
then ( Class ( the InternalRel of R,z) c= X & Class ( the InternalRel of R,z) c= Y ) by A1;
then ( z in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } & z in { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } ) ;
hence y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } by A1, XBOOLE_0:def 4; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } or y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } )
assume A2: y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } ; :: thesis: y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y }
then A3: y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } by XBOOLE_0:def 4;
A4: y in { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } by XBOOLE_0:def 4, A2;
consider z being Element of R such that
A5: ( z = y & Class ( the InternalRel of R,z) c= X ) by A3;
consider w being Element of R such that
A6: ( w = y & Class ( the InternalRel of R,w) c= Y ) by A4;
(Class ( the InternalRel of R,z)) /\ (Class ( the InternalRel of R,z)) c= X /\ Y by A5, XBOOLE_1:27, A6;
hence y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } by A5; :: thesis: verum

end;

hence LAp (X /\ Y) = (LAp X) /\ (LAp Y) ; :: thesis: verum