New approach for graph theory (continued)
New approach for graph theory (continued)

Main set.mm:
* theorem ~0ov added (several proofs shortened)
* theorems ~eqwrds3, ~wrdl3s3, ~s3sndisj, ~s3iunsndisj added

AV's mathbox:
* theorems ~wlksoneq1eq2, ~sPthis1wlk added
* definitions for WWalksNOn, WSPathsN, WSPathsNOn and related theorems added. These classes will replace the corresponding classes for walks/paths as ordered tripel. They are more general, better fitting to the concept of "walks as words", and have shorter representations  (<" a b c "> instead of <. a , b , c >.)
* section "Walks/paths of length 2 (as length 3 strings)" added (containing revised theorems of section "Walks/paths of length 2 as ordered triples  " and some theorems moved from section "Examples for walks, trails and paths "
* more revised theorems of section " Huneke's Proof of the Friendship Theorem"

metamath/set.mm,metamath/set.mm,metamath/set.mm