let V be non empty set ; :: thesis: for E being Relation of V holds
( E is irreflexive iff createGraph (V,E) is loopless )
let E be Relation of V; :: thesis: ( E is irreflexive iff createGraph (V,E) is loopless )

hereby :: thesis: ( createGraph (V,E) is loopless implies E is irreflexive )

assume E is irreflexive ; :: thesis: createGraph (V,E) is loopless
then VertexDomRel (createGraph (V,E)) is irreflexive ;
hence createGraph (V,E) is loopless ; :: thesis: verum

end;

assume createGraph (V,E) is loopless ; :: thesis: E is irreflexive
then VertexDomRel (createGraph (V,E)) is irreflexive ;
hence E is irreflexive ; :: thesis: verum