let Values be Values_with_Bool; :: thesis: for DS being DistributedSysWithSharedMem of Values
for e1, e2 being Event of DS holds
( e1 <= e2 or e2 <= e1 )
let DS be DistributedSysWithSharedMem of Values; :: thesis: for e1, e2 being Event of DS holds
( e1 <= e2 or e2 <= e1 )
let e1, e2 be Event of DS; :: thesis: ( e1 <= e2 or e2 <= e1 )
the events of DS is strongly_connected ;
then ( [e1,e2] in the InternalRel of the events of DS or [e2,e1] in the InternalRel of the events of DS ) by RELAT_2:def 7;
hence ( e1 <= e2 or e2 <= e1 ) by ORDERS_2:def 5; :: thesis: verum