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
Z1: CutLastLoc I c= J and
Z2: CutLastLoc J c= K ; :: according to COMPOS_2:def 4 :: thesis: I <= K
CutLastLoc I c= CutLastLoc J by Z1, Th18;
hence CutLastLoc I c= K by Z2, XBOOLE_1:1; :: according to COMPOS_2:def 4 :: thesis: verum