theorem Th71: :: GLUNIR00:71

for V being non empty set
for E being Relation of V holds
( ( E is total & E is reflexive ) iff createGraph (V,E) is loopfull )