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