:: deftheorem defines Segm ORDINAL1:def 17 :
for o being object holds Segm o = o;