Graphs being locally isomorphic but not isomorphic (2) (#4990)

* Local isomorphisms map triangles onto triangles

*  theorems moved from mathboxes to main: ~elrab2w,  ~elab2gw, ~elabgw, ~3rspcedvdw, ~fimarab
* new theorems in main: ~rexlimdvvva, ~f1ocoima
* new auxiliary theoems in AV's mathbox: ~3f1oss1, ~3f1oss2
* new theorems for closed neighborhoods in AV's mathbox: ~predgclnbgrel, ~clnbgredg, ~clnbgrssedg
* typo detected by GL fixed in section header "Triangles in graphs"
* new theorems for triangles in AV's mathbox: ~grtrimap
* new theorems for local isomorphisms between grahs in AV's mathbox: ~uspgrlim  (and lemmas), ~usgrlimprop, ~grlimgrtri

* Proof of ~grimgrtri shortened

* The example graphs ` H ` and ` G ` are not locally isomorphic

* Rewrap, lemmas renumbered

Author: avekens

changes-set.txt

@@ -92,6 +92,11 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+24-Aug-25 elrab2w   [same]      Moved from SN's mathbox to main set.mm
+24-Aug-25 elab2gw   [same]      Moved from SN's mathbox to main set.mm
+24-Aug-25 elabgw    [same]      Moved from SN's mathbox to main set.mm
+24-Aug-25 3rspcedvdw [same]     Moved from SN's mathbox to main set.mm
+24-Aug-25 fimarab   [same]      Moved from TA's mathbox to main set.mm
 20-Aug-25 naddsuc2  [same]      Moved from RP's mathbox to main set.mm
 18-Aug-25 cbvsumi   ---         deleted - redundant with cbvsum
 18-Aug-25 cbvsum    [same]      Removed unneeded hypotheses