let X be set ; :: thesis: for A1, A2 being SetSequence of X holds Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)
let A1, A2 be SetSequence of X; :: thesis: Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)
thus Intersection (A1 (/\) A2) c= (Intersection A1) /\ (Intersection A2) :: according to XBOOLE_0:def 10 :: thesis: (Intersection A1) /\ (Intersection A2) c= Intersection (A1 (/\) A2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection (A1 (/\) A2) or x in (Intersection A1) /\ (Intersection A2) )
assume A1: x in Intersection (A1 (/\) A2) ; :: thesis: x in (Intersection A1) /\ (Intersection A2)

now :: thesis: for k being Nat holds
( x in A1 . k & x in A2 . k )

let k be Nat; :: thesis: ( x in A1 . k & x in A2 . k )
x in (A1 (/\) A2) . k by A1, PROB_1:13;
then x in (A1 . k) /\ (A2 . k) by Def1;
hence ( x in A1 . k & x in A2 . k ) by XBOOLE_0:def 4; :: thesis: verum

end;

then ( x in Intersection A1 & x in Intersection A2 ) by PROB_1:13;
hence x in (Intersection A1) /\ (Intersection A2) by XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Intersection A1) /\ (Intersection A2) or x in Intersection (A1 (/\) A2) )
assume x in (Intersection A1) /\ (Intersection A2) ; :: thesis: x in Intersection (A1 (/\) A2)
then A2: ( x in Intersection A1 & x in Intersection A2 ) by XBOOLE_0:def 4;

now :: thesis: for k being Nat holds x in (A1 (/\) A2) . k

let k be Nat; :: thesis: x in (A1 (/\) A2) . k
( x in A1 . k & x in A2 . k ) by A2, PROB_1:13;
then x in (A1 . k) /\ (A2 . k) by XBOOLE_0:def 4;
hence x in (A1 (/\) A2) . k by Def1; :: thesis: verum

end;

hence x in Intersection (A1 (/\) A2) by PROB_1:13; :: thesis: verum