let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds
( ( E is total & E is reflexive ) iff G is loopfull )
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E holds
( ( E is total & E is reflexive ) iff G is loopfull )
let G be GraphFromSymRel of V,E; :: thesis: ( ( E is total & E is reflexive ) iff G is loopfull )
thus ( E is total & E is reflexive implies G is loopfull ) ; :: thesis: ( G is loopfull implies ( E is total & E is reflexive ) )
assume G is loopfull ; :: thesis: ( E is total & E is reflexive )
then createGraph (V,E) is loopfull ;
hence ( E is total & E is reflexive ) by Th71; :: thesis: verum