let X, Y1, Y2 be set ; :: thesis: UNION (X,(Y1 \/ Y2)) = (UNION (X,Y1)) \/ (UNION (X,Y2))
thus UNION (X,(Y1 \/ Y2)) c= (UNION (X,Y1)) \/ (UNION (X,Y2)) :: according to XBOOLE_0:def 10 :: thesis: (UNION (X,Y1)) \/ (UNION (X,Y2)) c= UNION (X,(Y1 \/ Y2))

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in UNION (X,(Y1 \/ Y2)) or xy in (UNION (X,Y1)) \/ (UNION (X,Y2)) )
assume A1: xy in UNION (X,(Y1 \/ Y2)) ; :: thesis: xy in (UNION (X,Y1)) \/ (UNION (X,Y2))
consider x, y being set such that
A2: ( x in X & y in Y1 \/ Y2 & xy = x \/ y ) by A1, SETFAM_1:def 4;
( y in Y1 or y in Y2 ) by A2, XBOOLE_0:def 3;
then ( xy in UNION (X,Y1) or xy in UNION (X,Y2) ) by A2, SETFAM_1:def 4;
hence xy in (UNION (X,Y1)) \/ (UNION (X,Y2)) by XBOOLE_0:def 3; :: thesis: verum

end;

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in (UNION (X,Y1)) \/ (UNION (X,Y2)) or xy in UNION (X,(Y1 \/ Y2)) )
assume A3: xy in (UNION (X,Y1)) \/ (UNION (X,Y2)) ; :: thesis: xy in UNION (X,(Y1 \/ Y2))

per cases ( xy in UNION (X,Y1) or xy in UNION (X,Y2) ) by A3, XBOOLE_0:def 3;

suppose xy in UNION (X,Y1) ; :: thesis: xy in UNION (X,(Y1 \/ Y2))

then consider x, y being set such that
A4: ( x in X & y in Y1 & xy = x \/ y ) by SETFAM_1:def 4;
y in Y1 \/ Y2 by A4, XBOOLE_0:def 3;
hence xy in UNION (X,(Y1 \/ Y2)) by A4, SETFAM_1:def 4; :: thesis: verum

end;

suppose xy in UNION (X,Y2) ; :: thesis: xy in UNION (X,(Y1 \/ Y2))

then consider x, y being set such that
A5: ( x in X & y in Y2 & xy = x \/ y ) by SETFAM_1:def 4;
y in Y1 \/ Y2 by A5, XBOOLE_0:def 3;
hence xy in UNION (X,(Y1 \/ Y2)) by A5, SETFAM_1:def 4; :: thesis: verum

end;

end;