defpred S₁[ object ] means $1 DSJoins X,Y,G;
consider IT being Subset of (the_Edges_of G) such that
A5: 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 DSJoins X,Y,G )
let e be object ; :: thesis: ( e in IT iff e DSJoins X,Y,G )
thus ( e in IT implies S₁[e] ) by A5; :: thesis: ( e DSJoins X,Y,G implies e in IT )
assume A6: e DSJoins X,Y,G ; :: thesis: e in IT
thus e in IT by A5, A6; :: thesis: verum