let G be _Graph; 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 ; 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 ; ( 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
; 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;