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

proof

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

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

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

end;

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

end;

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

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

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

end;

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