let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is loopfull implies G2 is loopfull )
assume G1 == G2 ; :: thesis: ( not G1 is loopfull or G2 is loopfull )
then G2 is reverseEdgeDirections of G1, {} by GLIB_009:42;
hence ( not G1 is loopfull or G2 is loopfull ) ; :: thesis: verum