let G be _finite _Graph; :: thesis:
let e be set ; :: thesis:
let v1, v2 be Vertex of G; :: thesis:
assume A1: e Joins v1,v2,G ; :: thesis:

per cases by A1, Th63;

suppose A2: ( e in v1 .edgesIn() & e in v2 .edgesOut() ) ; :: thesis:

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

end;

suppose A3: ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ; :: thesis:

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

end;

end;

end;

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