theorem :: COMPOS_2:25

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