let G be _Graph; :: thesis: for X1, X2 being set
for y being object holds G .edgesBetween ((X1 \/ X2),{y}) = (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))
let X1, X2 be set ; :: thesis: for y being object holds G .edgesBetween ((X1 \/ X2),{y}) = (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))
let y be object ; :: thesis: G .edgesBetween ((X1 \/ X2),{y}) = (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))
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 Th37;
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: ( e in G .edgesBetween ((X1 \/ X2),{y}) implies e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y})) )
assume e in G .edgesBetween ((X1 \/ X2),{y}) ; :: thesis: e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))
then e SJoins X1 \/ X2,{y},G by Def30;
then consider x being object such that
A2: ( x in X1 \/ X2 & e Joins x,y,G ) by Th102;
A3: y in {y} by TARSKI:def 1;

per cases ( x in X1 or x in X2 ) by A2, XBOOLE_0:def 3;

suppose x in X1 ; :: thesis: e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))

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

end;

suppose x in X2 ; :: thesis: e in (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))

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

end;

end;

end;

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