let Values be Values_with_Bool; :: thesis: for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for e1, e2 being Event of DS st e1 in p & e2 in p & e1 < e2 holds
e1 << e2
let DS be DistributedSysWithSharedMem of Values; :: thesis: for p being Process of DS
for e1, e2 being Event of DS st e1 in p & e2 in p & e1 < e2 holds
e1 << e2
let p be Process of DS; :: thesis: for e1, e2 being Event of DS st e1 in p & e2 in p & e1 < e2 holds
e1 << e2
let e1, e2 be Event of DS; :: thesis: ( e1 in p & e2 in p & e1 < e2 implies e1 << e2 )
assume A1: ( e1 in p & e2 in p ) ; :: thesis: ( not e1 < e2 or e1 << e2 )
assume A2: e1 < e2 ; :: thesis: e1 << e2
DS is consistent ;
then DS is pr-ordered ;
then ( not e1 <= e2 or not e2 <= e1 ) by A1, A2;
hence e1 << e2 by A2, ORDERS_2:def 6; :: thesis: verum