theorem Th23: :: COMPOS_2:23

for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S holds I <= I ';' J