let v be Vertex of G; :: thesis: not v is endvertex
assume v is endvertex ; :: thesis: contradiction
then A1: v .degree() = 1 by GLIB_000:174;

per cases ( c is infinite or c is finite ) ;

suppose A2: c is infinite ; :: thesis: contradiction

then G is c -regular ;
hence contradiction by A1, A2; :: thesis: verum

end;

suppose c is finite ; :: thesis: contradiction

then reconsider n = c as Nat ;
G is 2 * n -regular by Th46;
hence contradiction by A1, POLYFORM:4, ABIAN:def 2; :: thesis: verum

end;

end;