:: deftheorem defines Set_to_zero METRIC_1:def 20 :
Set_to_zero = [:2,2:] --> 0;