let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\) A1) c= A \ (Intersection A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds Intersection (A (\) A1) c= A \ (Intersection A1)
let A1 be SetSequence of X; :: thesis: Intersection (A (\) A1) c= A \ (Intersection A1)
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 & not x in A1 . k )

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

end;

then not x in A1 . 0 ;
then not x in Intersection A1 by PROB_1:13;
hence x in A \ (Intersection A1) by A2, XBOOLE_0:def 5; :: thesis: verum