:: deftheorem Def5 defines closed COMPOS_2:def 5 :
for S being with_non_trivial_Instructions COM-Struct
for I being preProgram of S holds
( I is closed iff for i being Instruction of S st i in rng I holds
rng (JumpPart i) c= dom I );