let G be _Graph; :: thesis: for X being set
for e, y being object st e SJoins X,{y},G holds
ex x being object st
( x in X & e Joins x,y,G )
let X be set ; :: thesis: for e, y being object st e SJoins X,{y},G holds
ex x being object st
( x in X & e Joins x,y,G )
let e, y be object ; :: thesis: ( e SJoins X,{y},G implies ex x being object st
( x in X & e Joins x,y,G ) )
assume A1: e SJoins X,{y},G ; :: thesis: ex x being object st
( x in X & e Joins x,y,G )
then A2: e in the_Edges_of G by GLIB_000:def 15;

per cases ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in {y} ) or ( (the_Source_of G) . e in {y} & (the_Target_of G) . e in X ) ) by A1, GLIB_000:def 15;

suppose A3: ( (the_Source_of G) . e in X & (the_Target_of G) . e in {y} ) ; :: thesis: ex x being object st
( x in X & e Joins x,y,G )

take (the_Source_of G) . e ; :: thesis: ( (the_Source_of G) . e in X & e Joins (the_Source_of G) . e,y,G )
(the_Target_of G) . e = y by A3, TARSKI:def 1;
then e DJoins (the_Source_of G) . e,y,G by A2, GLIB_000:def 14;
hence ( (the_Source_of G) . e in X & e Joins (the_Source_of G) . e,y,G ) by A3, GLIB_000:16; :: thesis: verum

end;

suppose A4: ( (the_Source_of G) . e in {y} & (the_Target_of G) . e in X ) ; :: thesis: ex x being object st
( x in X & e Joins x,y,G )

take (the_Target_of G) . e ; :: thesis: ( (the_Target_of G) . e in X & e Joins (the_Target_of G) . e,y,G )
(the_Source_of G) . e = y by A4, TARSKI:def 1;
then e DJoins y,(the_Target_of G) . e,G by A2, GLIB_000:def 14;
hence ( (the_Target_of G) . e in X & e Joins (the_Target_of G) . e,y,G ) by A4, GLIB_000:16; :: thesis: verum

end;

end;