let X be set ; :: thesis: for A1, A2 being SetSequence of X holds (Union A1) \ (Union A2) c= Union (A1 (\) A2)
let A1, A2 be SetSequence of X; :: thesis: (Union A1) \ (Union A2) c= Union (A1 (\) A2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union A1) \ (Union A2) or x in Union (A1 (\) A2) )
assume A1: x in (Union A1) \ (Union A2) ; :: thesis: x in Union (A1 (\) A2)
then x in Union A1 by XBOOLE_0:def 5;
then consider n1 being Nat such that
A2: x in A1 . n1 by PROB_1:12;
not x in Union A2 by A1, XBOOLE_0:def 5;
then not x in A2 . n1 by PROB_1:12;
then x in (A1 . n1) \ (A2 . n1) by A2, XBOOLE_0:def 5;
then x in (A1 (\) A2) . n1 by Def3;
hence x in Union (A1 (\) A2) by PROB_1:12; :: thesis: verum