let V be non empty set ; :: thesis: for E being Relation of V holds
( E is empty iff createGraph (V,E) is edgeless )
let E be Relation of V; :: thesis: ( E is empty iff createGraph (V,E) is edgeless )
thus ( E is empty implies createGraph (V,E) is edgeless ) ; :: thesis: ( createGraph (V,E) is edgeless implies E is empty )
assume createGraph (V,E) is edgeless ; :: thesis: E is empty
then VertexDomRel (createGraph (V,E)) is empty ;
hence E is empty ; :: thesis: verum