:: deftheorem defines L-Meas MEASUR14:def 10 :
for n being non zero Nat holds L-Meas n = (Seg n) --> L-Meas;