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