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