:: deftheorem defines PGraph JGRAPH_1:def 1 :
for X being set holds PGraph X = MultiGraphStruct(# X,[:X,X:],(pr1 (X,X)),(pr2 (X,X)) #);