:: deftheorem defines createGraph GLUNIR00:def 3 :
for V being non empty set
for E being Relation of V holds createGraph (V,E) = createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));