let V be non empty set ; :: thesis: for E being Relation of V
for e, v, w being object st e DJoins v,w, createGraph (V,E) holds
e = [v,w]
let E be Relation of V; :: thesis: for e, v, w being object st e DJoins v,w, createGraph (V,E) holds
e = [v,w]
let e, v, w be object ; :: thesis: ( e DJoins v,w, createGraph (V,E) implies e = [v,w] )
assume A1: e DJoins v,w, createGraph (V,E) ; :: thesis: e = [v,w]
then e in the_Edges_of (createGraph (V,E)) by GLIB_000:def 14;
then A2: e in E ;
then consider v1, w1 being object such that
A3: e = [v1,w1] by RELAT_1:def 1;
e DJoins v1,w1, createGraph (V,E) by A2, A3, Th63;
then ( v1 = v & w1 = w ) by A1, GLIB_000:125;
hence e = [v,w] by A3; :: thesis: verum