let x, y, z be Element of 2; :: thesis: Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z))
( Set_to_zero . (x,y) = 0 & Set_to_zero . (y,z) = 0 ) by Th27;
hence Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z)) by Th27; :: thesis: verum