let V be non empty set ; :: thesis: for E being Relation of V holds
( ( E is total & E is reflexive ) iff createGraph (V,E) is loopfull )
let E be Relation of V; :: thesis: ( ( E is total & E is reflexive ) iff createGraph (V,E) is loopfull )
set G = createGraph (V,E);
hereby :: thesis: ( createGraph (V,E) is loopfull implies ( E is total & E is reflexive ) )
assume ( E is total & E is reflexive ) ; :: thesis: createGraph (V,E) is loopfull
then id V c= E by ROUGHS_1:3;
then id (the_Vertices_of (createGraph (V,E))) c= E ;
then id (the_Vertices_of (createGraph (V,E))) c= VertexDomRel (createGraph (V,E)) ;
hence createGraph (V,E) is loopfull by Lm2; :: thesis: verum
end;
assume createGraph (V,E) is loopfull ; :: thesis: ( E is total & E is reflexive )
then id (the_Vertices_of (createGraph (V,E))) c= VertexDomRel (createGraph (V,E)) by Lm2;
then id (the_Vertices_of (createGraph (V,E))) c= E ;
then id V c= E ;
hence ( E is total & E is reflexive ) by ROUGHS_1:3; :: thesis: verum