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)

per cases ( ( x in A & not x in Union A1 ) or ( not x in A & x in Union A1 ) ) by A1, XBOOLE_0:1;

suppose A2: ( x in A & not x in Union A1 ) ; :: thesis: x in Union (A (\+\) A1)

then not x in A1 . 0 by PROB_1:12;
then x in A \+\ (A1 . 0) by A2, XBOOLE_0:1;
then x in (A (\+\) A1) . 0 by Def9;
hence x in Union (A (\+\) A1) by PROB_1:12; :: thesis: verum

end;

suppose A3: ( not x in A & x in Union A1 ) ; :: thesis: x in Union (A (\+\) A1)

then consider n1 being Nat such that
A4: x in A1 . n1 by PROB_1:12;
x in A \+\ (A1 . n1) by A3, A4, XBOOLE_0:1;
then x in (A (\+\) A1) . n1 by Def9;
hence x in Union (A (\+\) A1) by PROB_1:12; :: thesis: verum

end;

end;