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