take G = the 1 -vertex c -edge _Graph; :: thesis: ( G is _trivial & G is c -edge )
G .order() = 1 by Def3;
hence ( G is _trivial & G is c -edge ) by GLIB_000:def 19; :: thesis: verum