defpred S₁[ object ] means ex v being object st $1 Joins v,v,G;
consider L being Subset of (the_Edges_of G) such that
A1: for e being set holds
( e in L iff ( e in the_Edges_of G & S₁[e] ) ) from SUBSET_1:sch 1();
take L ; :: thesis: for e being object holds
( e in L iff ex v being object st e Joins v,v,G )
let e be object ; :: thesis: ( e in L iff ex v being object st e Joins v,v,G )
thus ( e in L implies ex v being object st e Joins v,v,G ) by A1; :: thesis: ( ex v being object st e Joins v,v,G implies e in L )
given v being object such that A2: e Joins v,v,G ; :: thesis: e in L
e in the_Edges_of G by A2, GLIB_000:def 13;
hence e in L by A1, A2; :: thesis: verum