let G be _finite non _trivial Tree-like _Graph; for v being Vertex of G st G .order() = 2 holds
v is endvertex
let v be Vertex of G; ( G .order() = 2 implies v is endvertex )
assume
G .order() = 2
; v is endvertex
then
card (the_Vertices_of G) = 2
by GLIB_000:def 24;
then consider v1, v2 being object such that
A1:
( v1 <> v2 & the_Vertices_of G = {v1,v2} )
by CARD_2:60;
consider w1, w2 being Vertex of G such that
A2:
( w1 <> w2 & w1 is endvertex & w2 is endvertex )
by GLIB_002:45;
( ( w1 = v1 or w1 = v2 ) & ( w2 = v1 or w2 = v2 ) )
by A1, TARSKI:def 2;
per cases then
( ( w1 = v1 & w2 = v2 ) or ( w1 = v2 & w2 = v1 ) )
by A2;
end;