for i being Element of I holds (I --> L) . i is antisymmetric by FUNCOP_1:7;
hence product (I --> L) is antisymmetric by WAYBEL_3:30; :: thesis: verum