let G be _Graph; :: thesis: ( G is edgeless iff G .size() = 0 )

hereby :: thesis: ( G .size() = 0 implies G is edgeless )

assume G is edgeless ; :: thesis: G .size() = 0
then card (the_Edges_of G) = 0 ;
hence G .size() = 0 by GLIB_000:def 25; :: thesis: verum

end;

assume G .size() = 0 ; :: thesis: G is edgeless
then card (the_Edges_of G) = 0 by GLIB_000:def 25;
hence G is edgeless ; :: thesis: verum