rus:Пусть x - фигура. x есть ребро еите x инцидентна какой-то фигуре.
yfl:declaration edge func(TV U) (x) ≝ (∃y:U (x inc y)).
Замечание. Легко видеть что понятие ребра как встречающегося слева может быть введено для произвольного ботн. В произвольном бинарном отношении называть элемент встречающийся слева ребром – смело до неадеквата;-) ибо настоящим ребром его делают свойства INC01-2, но практика говорить «это ребро» вместо «это встречается слева» симпатична.
(тип функции в Y!L):в "func(TV U)" применено «обратное перечисление» типов аргументов и результата в типе функции: TV – тип результата! В обычной записи типа функции мы имели бы U:TV.