let G1 be reverseEdgeDirections of G,X; :: thesis: G1 is edgeless

per cases ( X c= the_Edges_of G or not X c= the_Edges_of G ) ;

suppose X c= the_Edges_of G ; :: thesis: G1 is edgeless

hence G1 is edgeless by GLIB_007:def 1; :: thesis: verum

end;

suppose not X c= the_Edges_of G ; :: thesis: G1 is edgeless

then G1 == G by GLIB_007:def 1;
then the_Edges_of G1 = the_Edges_of G by GLIB_000:def 34;
hence G1 is edgeless ; :: thesis: verum

end;

end;