2. in : |R|
IdLnk
3. out : |R|
IdLnk
4. j : Id
5. R(j)
6.
i:|R|.
6. R(source(in(i))) & R(destination(out(i)))
6. & source(out(i)) = i
6. & & destination(in(i)) = i
6. & & in(destination(out(i))) = out(i)
6. & & out(source(in(i))) = in(i)
7.
i,j:|R|. 
k:
. 
x.destination(out(x))^k(i) = j
8. |R|
9. R(source(in(j)))
10. R(destination(out(j)))
11. source(out(j)) = j
12. destination(in(j)) = j
13. in(destination(out(j))) = out(j)
14. out(source(in(j))) = in(j)
15. z : IdLnk
16. z = in(j)
R(destination(in(j)))
