defpred S₁[ set ] 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 set holds
( e in IT iff e SJoins X,Y,G )
let e be set ; :: 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
then e in the_Edges_of G by Def17;
hence e in IT by A1, A2; :: thesis: verum