let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds A \ (Union A1) c= Union (A (\) A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds A \ (Union A1) c= Union (A (\) A1)
let A1 be SetSequence of X; :: thesis: A \ (Union A1) c= Union (A (\) A1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ (Union A1) or x in Union (A (\) A1) )
assume A1: x in A \ (Union A1) ; :: thesis: x in Union (A (\) A1)
then A2: not x in Union A1 by XBOOLE_0:def 5;

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 & not x in A1 . k ) by A1, A2, PROB_1:12, XBOOLE_0:def 5;
then x in A \ (A1 . k) by XBOOLE_0:def 5;
hence x in (A (\) A1) . k by Def7; :: thesis: verum

end;

then x in (A (\) A1) . 1 ;
hence x in Union (A (\) A1) by PROB_1:12; :: thesis: verum