:: deftheorem defines <= COMPOS_2:def 4 :
for I being non empty NAT -defined finite Function
for J being set holds
( I <= J iff CutLastLoc I c= J );