let x, y, z be Element of 1; Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z)))
A1:
z = {}
by CARD_1:49, TARSKI:def 1;
( x = {} & y = {} )
by CARD_1:49, TARSKI:def 1;
hence
Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z)))
by A1; verum