hereby :: thesis: ( v .degree() = 1 implies v is endvertex )

assume v is endvertex ; :: thesis: v .degree() = 1
then consider e being object such that
A1: v .edgesInOut() = {e} and
A2: not e Joins v,v,G ;

now :: thesis: v .degree() = 1

per cases ( ( v .edgesIn() = {e} & v .edgesOut() = {e} ) or ( v .edgesIn() = {} & v .edgesOut() = {e} ) or ( v .edgesIn() = {e} & v .edgesOut() = {} ) ) by A1, ZFMISC_1:37;

suppose A3: ( v .edgesIn() = {e} & v .edgesOut() = {e} ) ; :: thesis: v .degree() = 1

then e in v .edgesOut() by TARSKI:def 1;
then A4: (the_Source_of G) . e = v by Lm8;
A5: e in v .edgesIn() by A3, TARSKI:def 1;
then (the_Target_of G) . e = v by Lm7;
hence v .degree() = 1 by A2, A5, A4; :: thesis: verum

end;

suppose ( v .edgesIn() = {} & v .edgesOut() = {e} ) ; :: thesis: v .degree() = 1

hence v .degree() = 1 by CARD_1:30; :: thesis: verum

end;

suppose ( v .edgesIn() = {e} & v .edgesOut() = {} ) ; :: thesis: v .degree() = 1

hence v .degree() = 1 by CARD_1:30; :: thesis: verum

end;

end;

end;

hence v .degree() = 1 ; :: thesis: verum

end;

assume A6: v .degree() = 1 ; :: thesis: v is endvertex

now :: thesis: v is endvertex

per cases ( card (v .edgesIn()) = 0 or card (v .edgesIn()) <> 0 ) ;

suppose A7: card (v .edgesIn()) = 0 ; :: thesis: v is endvertex

then consider e being object such that
A8: v .edgesOut() = {e} by A6, CARD_2:42;
A9: v .edgesIn() = {} by A7;
then A10: not e Joins v,v,G by Lm7;
v .edgesInOut() = {e} by A9, A8;
hence v is endvertex by A10; :: thesis: verum

end;

suppose card (v .edgesIn()) <> 0 ; :: thesis: v is endvertex

then 0 < card (v .edgesIn()) ;
then A11: 0 + 1 <= card (v .edgesIn()) by NAT_1:13;
card (v .edgesIn()) <= 1 by A6, NAT_1:11;
then A12: card (v .edgesIn()) = 1 by A11, XXREAL_0:1;
then consider e being object such that
A13: v .edgesIn() = {e} by CARD_2:42;
A14: v .edgesOut() = {} by A6, A12;
then A15: not e Joins v,v,G by Lm8;
v .edgesInOut() = {e} by A13, A14;
hence v is endvertex by A15; :: thesis: verum

end;

end;

end;

hence v is endvertex ; :: thesis: verum