for i being Element of I holds (I --> L) . i is transitive ;
hence product (I --> L) is transitive by WAYBEL_3:29; :: thesis: verum