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)
A1: ( (Union A1) \ (Union A2) c= Union (A1 (\) A2) & (Union A2) \ (Union A1) c= Union (A2 (\) A1) ) by Th10;
(Union (A1 (\) A2)) \/ (Union (A2 (\) A1)) = Union ((A1 (\) A2) (\/) (A2 (\) A1)) by Th9
.= Union (A1 (\+\) A2) by Th3 ;
hence (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2) by A1, XBOOLE_1:13; :: thesis: verum