theorem Th130: :: GLIBPRE1:127

for V being non empty set
for E being Relation of V holds (createGraph (V,E)) .loops() = E /\ (id V)