per cases ( ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) or for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) ;

suppose A1: ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) ; :: thesis: Weight v1,v2,W is Real

then consider e being set such that
A2: ( XEdge v1,v2 = e & e in the carrier' of G & e orientedly_joins v1,v2 ) by Def6;
e in dom W by A2, FUNCT_2:def 1;
then W . (XEdge v1,v2) in Real>=0 by A2, PARTFUN1:27;
hence Weight v1,v2,W is Real by A1, Def7; :: thesis: verum

end;

suppose for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ; :: thesis: Weight v1,v2,W is Real

hence Weight v1,v2,W is Real by Def7; :: thesis: verum

end;

end;