theorem :: COMPOS_2:19

for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S
for K being set st I <= J & J <= K holds
I <= K