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

( 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