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