theorem Th64: :: GLUNIR00:64

for V being non empty set
for E being Relation of V
for e, v, w being object st e DJoins v,w, createGraph (V,E) holds
e = [v,w]