:: deftheorem Def7 defines ins-loc-free COMPOS_0:def 8 :
for S being standard-ins set
for I being Element of S holds
( I is ins-loc-free iff JumpPart I is empty );