let x, y, z be Element of 1; :: thesis: op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z))
( x = {} & y = {} ) by CARD_1:49, TARSKI:def 1;
hence op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z)) by Lm2; :: thesis: verum