let G be edgeless _Graph; :: thesis: 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 ; :: thesis: ( not e Joins v1,v2,G & not e DJoins v1,v2,G )
not e Joins v1,v2,G
proof
assume e Joins v1,v2,G ; :: thesis: contradiction
then e in the_Edges_of G by GLIB_000:def 13;
hence contradiction ; :: thesis: verum
end;
hence ( not e Joins v1,v2,G & not e DJoins v1,v2,G ) by GLIB_000:16; :: thesis: verum