let Values be Values_with_Bool; :: thesis: for DS being DistributedSysWithSharedMem of Values
for e1, e2, e3 being Event of DS st e1 <= e2 & e2 <= e3 holds
e1 <= e3
let DS be DistributedSysWithSharedMem of Values; :: thesis: for e1, e2, e3 being Event of DS st e1 <= e2 & e2 <= e3 holds
e1 <= e3
let e1, e2, e3 be Event of DS; :: thesis: ( e1 <= e2 & e2 <= e3 implies e1 <= e3 )
( [e1,e2] in the InternalRel of the events of DS & [e2,e3] in the InternalRel of the events of DS implies [e1,e3] in the InternalRel of the events of DS ) by ORDERS_2:def 3, RELAT_2:def 8;
hence ( e1 <= e2 & e2 <= e3 implies e1 <= e3 ) by ORDERS_2:def 5; :: thesis: verum