let G be _Graph; :: thesis: ( ex v being Vertex of G st v is endvertex implies not G is _trivial )
given v being Vertex of G such that A1: v is endvertex ; :: thesis: not G is _trivial
set G2 = the removeVertex of G,v;
consider e being object such that
A2: ( v .edgesInOut() = {e} & not e Joins v,v,G ) by A1;
set w = v .adj e;
A3: e in v .edgesInOut() by A2, TARSKI:def 1;
for u being Vertex of G holds the_Vertices_of G <> {u}

proof

let u be Vertex of G; :: thesis: the_Vertices_of G <> {u}
assume the_Vertices_of G = {u} ; :: thesis: contradiction
then ( v = u & v .adj e = u ) by TARSKI:def 1;
hence contradiction by A2, A3, Th67; :: thesis: verum

end;

hence not G is _trivial by Th22; :: thesis: verum