l1,l2,l3:T List. l2 
l3 
l1 l2 l1 l3l1,l2,l3:T List. l1 l2 l2 l3 l1 l3| Theorem | Name |
| l1,l2,l3:T List. l2 l3 l1 l2 l1 l3 | [iseg_transitivity2] |
| cites the following: | |
| l1,l2,l3:T List. l1 l2 l2 l3 l1 l3 | [iseg_transitivity] |