let IT1, IT2 be Subset of (the_Edges_of G); :: thesis: ( ( for e being set holds
( e in IT1 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ) & ( for e being set holds
( e in IT2 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ) implies IT1 = IT2 )
assume that
A3: for e being set holds
( e in IT1 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) and
A4: for e being set holds
( e in IT2 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ; :: thesis: IT1 = IT2

now :: thesis: for e being object holds
( ( e in IT1 implies e in IT2 ) & ( e in IT2 implies e in IT1 ) )

let e be object ; :: thesis: ( ( e in IT1 implies e in IT2 ) & ( e in IT2 implies e in IT1 ) )
reconsider ee = e as set by TARSKI:1;

hereby :: thesis: ( e in IT2 implies e in IT1 )

assume e in IT1 ; :: thesis: e in IT2
then ( ee is_forward_edge_wrt VL or ee is_backward_edge_wrt VL ) by A3;
hence e in IT2 by A4; :: thesis: verum

end;

assume e in IT2 ; :: thesis: e in IT1
then ( ee is_forward_edge_wrt VL or ee is_backward_edge_wrt VL ) by A4;
hence e in IT1 by A3; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum