:: deftheorem defines ZeroSpace METRIC_1:def 21 :
ZeroSpace = MetrStruct(# 2,Set_to_zero #);