for G being Graph
for U, V being set
for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & v2 in V & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
for p being oriented Chain of G holds not p is_orientedpath_of v1,v2