is mentioned by

Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((inverse(e)  from(i))  destination(e) = i)	[edge-inv-from]
Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((inverse(e)  to(i))  source(e) = i)	[edge-inv-to]
Def spanner(f;T;to;from) Def == (l:Edge(T). f(l) = f(inverse(l))) Def == & (i:|T|, l1,l2:Edge(T). Def == & ((l1  to(i)) Def == & ( Def == & ((l2  to(i))  l1 = l2  IdLnk  (f(l1))  (f(l2)))	[spanner]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html