let G be finite _Graph; :: thesis: for e being set
for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( 1 <= v1 .degree() & 1 <= v2 .degree() )
let e be set ; :: thesis: for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( 1 <= v1 .degree() & 1 <= v2 .degree() )
let v1, v2 be Vertex of G; :: thesis: ( e Joins v1,v2,G implies ( 1 <= v1 .degree() & 1 <= v2 .degree() ) )
assume A1: e Joins v1,v2,G ; :: thesis: ( 1 <= v1 .degree() & 1 <= v2 .degree() )

now

per cases ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) by A1, Th66;

suppose A2: ( e in v1 .edgesIn() & e in v2 .edgesOut() ) ; :: thesis: ( 1 <= v1 .degree() & 1 <= v2 .degree() )

then for x being set st x in {e} holds
x in v1 .edgesIn() by TARSKI:def 1;
then {e} c= v1 .edgesIn() by TARSKI:def 3;
then card {e} <= card (v1 .edgesIn() ) by NAT_1:44;
then 1 <= v1 .inDegree() by CARD_1:50;
hence 1 <= v1 .degree() by NAT_1:12; :: thesis: 1 <= v2 .degree()
for x being set st x in {e} holds
x in v2 .edgesOut() by A2, TARSKI:def 1;
then {e} c= v2 .edgesOut() by TARSKI:def 3;
then card {e} <= card (v2 .edgesOut() ) by NAT_1:44;
then 1 <= v2 .outDegree() by CARD_1:50;
hence 1 <= v2 .degree() by NAT_1:12; :: thesis: verum

end;

suppose A3: ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ; :: thesis: ( 1 <= v1 .degree() & 1 <= v2 .degree() )

then for x being set st x in {e} holds
x in v1 .edgesOut() by TARSKI:def 1;
then {e} c= v1 .edgesOut() by TARSKI:def 3;
then card {e} <= card (v1 .edgesOut() ) by NAT_1:44;
then 1 <= v1 .outDegree() by CARD_1:50;
hence 1 <= v1 .degree() by NAT_1:12; :: thesis: 1 <= v2 .degree()
for x being set st x in {e} holds
x in v2 .edgesIn() by A3, TARSKI:def 1;
then {e} c= v2 .edgesIn() by TARSKI:def 3;
then card {e} <= card (v2 .edgesIn() ) by NAT_1:44;
then 1 <= v2 .inDegree() by CARD_1:50;
hence 1 <= v2 .degree() by NAT_1:12; :: thesis: verum

end;

end;

end;

hence ( 1 <= v1 .degree() & 1 <= v2 .degree() ) ; :: thesis: verum