let G be edgeless _Graph; for e, v1, v2 being object holds
( not e Joins v1,v2,G & not e DJoins v1,v2,G )
let e, v1, v2 be object ; ( not e Joins v1,v2,G & not e DJoins v1,v2,G )
not e Joins v1,v2,G
hence
( not e Joins v1,v2,G & not e DJoins v1,v2,G )
by GLIB_000:16; verum