defpred S₁[ object ] means $1 SJoins X,Y,G;
consider IT being Subset of (the_Edges_of G) such that
A1: for e being set holds
( e in IT iff ( e in the_Edges_of G & S₁[e] ) ) from SUBSET_1:sch 1();
take IT ; :: thesis: for e being object holds
( e in IT iff e SJoins X,Y,G )
let e be object ; :: thesis: ( e in IT iff e SJoins X,Y,G )
thus ( e in IT implies S₁[e] ) by A1; :: thesis: ( e SJoins X,Y,G implies e in IT )
assume A2: e SJoins X,Y,G ; :: thesis: e in IT
thus e in IT by A1, A2; :: thesis: verum