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