theorem :: COMPOS_2:22

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