let G be _Graph; :: thesis:
let X1, X2 be set ; :: thesis:
let y be object ; :: thesis:
set E1 = G .edgesBetween (X1,{y});
set E2 = G .edgesBetween (X2,{y});
( X1 c= X1 \/ X2 & X2 c= X1 \/ X2 ) by XBOOLE_1:7;
then ( G .edgesBetween (X1,{y}) c= G .edgesBetween ((X1 \/ X2),{y}) & G .edgesBetween (X2,{y}) c= G .edgesBetween ((X1 \/ X2),{y}) ) by GLIB_000:37;
then A1: (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y})) c= G .edgesBetween ((X1 \/ X2),{y}) by XBOOLE_1:8;
for e being object st e in G .edgesBetween ((X1 \/ X2),{y}) holds
e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))

proof

let e be object ; :: thesis:
assume e in G .edgesBetween ((X1 \/ X2),{y}) ; :: thesis:
then e SJoins X1 \/ X2,{y},G by GLIB_000:def 30;
then consider x being object such that
A2: ( x in X1 \/ X2 & e Joins x,y,G ) by Th21;
A3: y in {y} by TARSKI:def 1;

per cases by A2, XBOOLE_0:def 3;

suppose x in X1 ; :: thesis:

then e SJoins X1,{y},G by A2, A3, GLIB_000:17;
then e in G .edgesBetween (X1,{y}) by GLIB_000:def 30;
hence e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y})) by XBOOLE_0:def 3; :: thesis:

end;

suppose x in X2 ; :: thesis:

then e SJoins X2,{y},G by A2, A3, GLIB_000:17;
then e in G .edgesBetween (X2,{y}) by GLIB_000:def 30;
hence e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y})) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then G .edgesBetween ((X1 \/ X2),{y}) c= (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y})) by TARSKI:def 3;
hence G .edgesBetween ((X1 \/ X2),{y}) = (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y})) by A1, XBOOLE_0:def 10; :: thesis: