let G be edgeless _Graph; :: thesis: for e being object
for X, Y being set holds
( not e SJoins X,Y,G & not e DSJoins X,Y,G )
let e be object ; :: thesis: for X, Y being set holds
( not e SJoins X,Y,G & not e DSJoins X,Y,G )
let X, Y be set ; :: thesis: ( not e SJoins X,Y,G & not e DSJoins X,Y,G )
thus not e SJoins X,Y,G :: thesis: not e DSJoins X,Y,G
proof
assume e SJoins X,Y,G ; :: thesis: contradiction
then e in the_Edges_of G by GLIB_000:def 15;
hence contradiction ; :: thesis: verum
end;
thus not e DSJoins X,Y,G :: thesis: verum
proof
assume e DSJoins X,Y,G ; :: thesis: contradiction
then e in the_Edges_of G by GLIB_000:def 16;
hence contradiction ; :: thesis: verum
end;