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 object ; :: 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= Y by Th8, XBOOLE_1:18;
then A2: x in LAp Y by A1;
Class ( the InternalRel of A,x) c= X by A1, Th8, XBOOLE_1:18;
then x in LAp X by A1;
hence x in (LAp X) /\ (LAp Y) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

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