theorem :: GRAPH_1:26

for G1 being Graph
for G being non-multi Graph st G1 c= G holds
G1 is non-multi