let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A1 (\) A) = (Intersection A1) \ A
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds Intersection (A1 (\) A) = (Intersection A1) \ A
let A1 be SetSequence of X; :: thesis: Intersection (A1 (\) A) = (Intersection A1) \ A
thus Intersection (A1 (\) A) c= (Intersection A1) \ A :: according to XBOOLE_0:def 10 :: thesis: (Intersection A1) \ A c= Intersection (A1 (\) A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection (A1 (\) A) or x in (Intersection A1) \ A )
assume A1: x in Intersection (A1 (\) A) ; :: thesis: x in (Intersection A1) \ A
A2: now :: thesis: for k being Nat holds
( x in A1 . k & not x in A )
let k be Nat; :: thesis: ( x in A1 . k & not x in A )
x in (A1 (\) A) . k by A1, PROB_1:13;
then x in (A1 . k) \ A by Def8;
hence ( x in A1 . k & not x in A ) by XBOOLE_0:def 5; :: thesis: verum
end;
then x in Intersection A1 by PROB_1:13;
hence x in (Intersection A1) \ A by A2, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Intersection A1) \ A or x in Intersection (A1 (\) A) )
assume A3: x in (Intersection A1) \ A ; :: thesis: x in Intersection (A1 (\) A)
then A4: x in Intersection A1 by XBOOLE_0:def 5;
now :: thesis: for k being Nat holds x in (A1 (\) A) . k
let k be Nat; :: thesis: x in (A1 (\) A) . k
( x in A1 . k & not x in A ) by A3, A4, PROB_1:13, XBOOLE_0:def 5;
then x in (A1 . k) \ A by XBOOLE_0:def 5;
hence x in (A1 (\) A) . k by Def8; :: thesis: verum
end;
hence x in Intersection (A1 (\) A) by PROB_1:13; :: thesis: verum