theorem :: COMPOS_2:24

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