let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I, J being MacroInstruction of S st I <= J & J <= I holds
I = J
let I, J be MacroInstruction of S; :: thesis: ( I <= J & J <= I implies I = J )
assume CutLastLoc I c= J ; :: according to COMPOS_2:def 4 :: thesis: ( not J <= I or I = J )
then A1: CutLastLoc I c= CutLastLoc J by Th18;
assume CutLastLoc J c= I ; :: according to COMPOS_2:def 4 :: thesis: I = J
then CutLastLoc J c= CutLastLoc I by Th18;
then CutLastLoc I = CutLastLoc J by A1, XBOOLE_0:def 10;
hence I = J by Th21; :: thesis: verum