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