let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I, J being MacroInstruction of S st I <= J holds
for X being set st J c= X holds
I <= X
let I, J be MacroInstruction of S; :: thesis: ( I <= J implies for X being set st J c= X holds
I <= X )
assume A1: CutLastLoc I c= J ; :: according to COMPOS_2:def 4 :: thesis: for X being set st J c= X holds
I <= X
let X be set ; :: thesis: ( J c= X implies I <= X )
assume J c= X ; :: thesis: I <= X
hence CutLastLoc I c= X by A1; :: according to COMPOS_2:def 4 :: thesis: verum