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

assume v is endvertex ; :: thesis: v .degree() = 1
then consider e being set such that
A1: ( v .edgesInOut() = {e} & not e Joins v,v,G ) by Def53;

now

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

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

then A2: ( e in v .edgesIn() & e in v .edgesOut() ) by TARSKI:def 1;
then A3: ( e in the_Edges_of G & (the_Target_of G) . e = v ) by Lm8;
(the_Source_of G) . e = v by A2, Lm9;
hence v .degree() = 1 by A1, A3, Def15; :: thesis: verum

end;

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

hence v .degree() = 1 by CARD_1:47, CARD_1:50; :: thesis: verum

end;

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

hence v .degree() = 1 by CARD_1:47, CARD_1:50; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

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

then A6: v .edgesIn() = {} ;
consider e being set such that
A7: v .edgesOut() = {e} by A4, A5, CARD_2:60;
A8: v .edgesInOut() = {e} by A6, A7;

now

assume e Joins v,v,G ; :: thesis: contradiction
then ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by Def15;
hence contradiction by A6, Lm8; :: thesis: verum

end;

hence v is endvertex by A8, Def53; :: thesis: verum

end;

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

then 0 < card (v .edgesIn() ) by NAT_1:3;
then A9: 0 + 1 <= card (v .edgesIn() ) by NAT_1:13;
card (v .edgesIn() ) <= 1 by A4, NAT_1:11;
then A10: card (v .edgesIn() ) = 1 by A9, XXREAL_0:1;
then consider e being set such that
A11: v .edgesIn() = {e} by CARD_2:60;
A12: v .edgesOut() = {} by A4, A10;
then A13: v .edgesInOut() = {e} by A11;

now

assume e Joins v,v,G ; :: thesis: contradiction
then ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by Def15;
hence contradiction by A12, Lm9; :: thesis: verum

end;

hence v is endvertex by A13, Def53; :: thesis: verum

end;

end;

end;

hence v is endvertex ; :: thesis: verum