let G be _Graph; :: thesis: for v being Vertex of G holds
( v is endvertex iff v .degree() = 1 )
let v be Vertex of G; :: thesis: ( v is endvertex iff v .degree() = 1 )

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} & not e Joins v,v,G ) ;
e in v .edgesInOut() by A1, TARSKI:def 1;

per cases then ( e in v .edgesIn() or e in v .edgesOut() ) by XBOOLE_0:def 3;

suppose A2: e in v .edgesIn() ; :: thesis: v .degree() = 1

then consider w being set such that
A3: e DJoins w,v,G by Th57;
(the_Source_of G) . e <> v by A1, A3;
then not e in v .edgesOut() by Lm8;
then A4: not {e} c= v .edgesOut() by ZFMISC_1:31;
( v .edgesIn() c= {e} & v .edgesOut() c= {e} ) by A1, XBOOLE_1:7;
then ( v .edgesIn() = {e} & v .edgesOut() = {} ) by A2, A4, ZFMISC_1:33;
hence v .degree() = (card 1) +` (card 0) by CARD_1:30
.= card (1 + 0) by CARD_2:38
.= 1 ;
:: thesis: verum

end;

suppose A5: e in v .edgesOut() ; :: thesis: v .degree() = 1

then consider w being set such that
A6: e DJoins v,w,G by Th59;
(the_Target_of G) . e <> v by A1, A6;
then not e in v .edgesIn() by Lm7;
then A7: not {e} c= v .edgesIn() by ZFMISC_1:31;
( v .edgesIn() c= {e} & v .edgesOut() c= {e} ) by A1, XBOOLE_1:7;
then ( v .edgesIn() = {} & v .edgesOut() = {e} ) by A5, A7, ZFMISC_1:33;
hence v .degree() = (card 1) +` (card 0) by CARD_1:30
.= card (1 + 0) by CARD_2:38
.= 1 ;
:: thesis: verum

end;

end;

end;

assume A8: v .degree() = 1 ; :: thesis: v is endvertex
( ( v .inDegree() = 1 & v .outDegree() = 0 ) or ( v .inDegree() = 0 & v .outDegree() = 1 ) )

proof

assume ( not v .inDegree() = 1 or not v .outDegree() = 0 ) ; :: thesis: ( v .inDegree() = 0 & v .outDegree() = 1 )

per cases then ( v .inDegree() <> 1 or v .outDegree() <> 0 ) ;

suppose A9: v .inDegree() <> 1 ; :: thesis: ( v .inDegree() = 0 & v .outDegree() = 1 )

v .inDegree() c= 1 by A8, CARD_2:94;
then not 1 c= v .inDegree() by A9, XBOOLE_0:def 10;
then v .inDegree() in 1 by ORDINAL1:16;
hence v .inDegree() = 0 by CARD_1:49, TARSKI:def 1; :: thesis: v .outDegree() = 1
hence v .outDegree() = 1 by A8, CARD_2:18; :: thesis: verum

end;

suppose v .outDegree() <> 0 ; :: thesis: ( v .inDegree() = 0 & v .outDegree() = 1 )

then not v .outDegree() in 1 by CARD_1:49, TARSKI:def 1;
then A10: 1 c= v .outDegree() by ORDINAL1:16;
v .outDegree() c= 1 by A8, CARD_2:94;
then A11: v .outDegree() = 1 by A10, XBOOLE_0:def 10;

hereby :: thesis: v .outDegree() = 1

assume v .inDegree() <> 0 ; :: thesis: contradiction
then not v .inDegree() in 1 by CARD_1:49, TARSKI:def 1;
then A12: 1 c= v .inDegree() by ORDINAL1:16;
v .inDegree() c= 1 by A8, CARD_2:94;
then (v .inDegree()) +` (v .outDegree()) = (card 1) +` (card 1) by A11, A12, XBOOLE_0:def 10
.= card (1 + 1) by CARD_2:38
.= 2 ;
hence contradiction by A8; :: thesis: verum

end;

thus v .outDegree() = 1 by A11; :: thesis: verum

end;

end;

end;

per cases then ( ( v .inDegree() = 1 & v .outDegree() = 0 ) or ( v .inDegree() = 0 & v .outDegree() = 1 ) ) ;

suppose A13: ( v .inDegree() = 1 & v .outDegree() = 0 ) ; :: thesis: v is endvertex

then v .inDegree() = card {{}} by CARD_1:30;
then consider e being object such that
A14: v .edgesIn() = {e} by CARD_1:29;
v .edgesOut() = {} by A13;
then A15: v .edgesInOut() = {e} by A14;
not e Joins v,v,G

proof

assume e Joins v,v,G ; :: thesis: contradiction
then ( e DJoins v,v,G & e is set ) ;
then e in v .edgesOut() by Th59;
hence contradiction by A13; :: thesis: verum

end;

hence v is endvertex by A15; :: thesis: verum

end;

suppose A16: ( v .inDegree() = 0 & v .outDegree() = 1 ) ; :: thesis: v is endvertex

then v .outDegree() = card {{}} by CARD_1:30;
then consider e being object such that
A17: v .edgesOut() = {e} by CARD_1:29;
v .edgesIn() = {} by A16;
then A18: v .edgesInOut() = {e} by A17;
not e Joins v,v,G

proof

assume e Joins v,v,G ; :: thesis: contradiction
then ( e DJoins v,v,G & e is set ) ;
then e in v .edgesIn() by Th57;
hence contradiction by A16; :: thesis: verum

end;

hence v is endvertex by A18; :: thesis: verum

end;

end;