let A be Tolerance_Space; :: thesis: for X, Y being Subset of A holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)
let X, Y be Subset of A; :: thesis: LAp (X /\ Y) = (LAp X) /\ (LAp Y)
thus LAp (X /\ Y) c= (LAp X) /\ (LAp Y) :: according to XBOOLE_0:def 10 :: thesis: (LAp X) /\ (LAp Y) c= LAp (X /\ Y)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LAp (X /\ Y) or x in (LAp X) /\ (LAp Y) )
assume A1: x in LAp (X /\ Y) ; :: thesis: x in (LAp X) /\ (LAp Y)
then ( Class the InternalRel of A,x c= X & Class the InternalRel of A,x c= Y ) by Th8, XBOOLE_1:18;
then ( x in LAp X & x in LAp Y ) by A1;
hence x in (LAp X) /\ (LAp Y) by XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LAp X) /\ (LAp Y) or x in LAp (X /\ Y) )
assume A2: x in (LAp X) /\ (LAp Y) ; :: thesis: x in LAp (X /\ Y)
then ( x in LAp X & x in LAp Y ) by XBOOLE_0:def 4;
then ( Class the InternalRel of A,x c= X & Class the InternalRel of A,x c= Y ) by Th8;
then Class the InternalRel of A,x c= X /\ Y by XBOOLE_1:19;
hence x in LAp (X /\ Y) by A2; :: thesis: verum