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 ) ) ;

end;

( 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

( 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 and

A3: e in the carrier' of G and

e orientedly_joins v1,v2 by Def6;

e in dom W by A3, FUNCT_2:def 1;

then W . (XEdge (v1,v2)) in Real>=0 by A2, PARTFUN1:4;

hence Weight (v1,v2,W) is real by A1, Def7; :: thesis: verum

end;A2: XEdge (v1,v2) = e and

A3: e in the carrier' of G and

e orientedly_joins v1,v2 by Def6;

e in dom W by A3, FUNCT_2:def 1;

then W . (XEdge (v1,v2)) in Real>=0 by A2, PARTFUN1:4;

hence Weight (v1,v2,W) is real by A1, Def7; :: thesis: verum

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

end;

( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ; :: thesis: Weight (v1,v2,W) is real

end;