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

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;