∀x,j,i:Top.  (source(link_x from i to j) ~ i)
{ (UnivCD THENA Auto) }
1. x : Top@i
2. j : Top@i
3. i : Top@i
⊢ source(link_x from i to j) ~ i