defpred S_{1}[ 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_{1}[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

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

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