defpred S₁[ set ] means ( $1 is_forward_edge_wrt VL or $1 is_backward_edge_wrt VL );
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 is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) )
let e be set ; :: thesis: ( e in IT iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) )
thus ( e in IT implies S₁[e] ) by A1; :: thesis: ( ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) implies e in IT )
assume A2: S₁[e] ; :: thesis: e in IT
then e in the_Edges_of G by Def6, Def7;
hence e in IT by A1, A2; :: thesis: verum