let Values be Values_with_Bool; :: thesis: for DS being DistributedSysWithSharedMem of Values

for p being Process of DS

for tr being trace of DS

for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let DS be DistributedSysWithSharedMem of Values; :: thesis: for p being Process of DS

for tr being trace of DS

for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let p be Process of DS; :: thesis: for tr being trace of DS

for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let tr be trace of DS; :: thesis: for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let e1, e2 be Event of DS; :: thesis: (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (e1,e2) interval_in (p,tr) or o in (e1,e2) inter )

assume O1: o in (e1,e2) interval_in (p,tr) ; :: thesis: o in (e1,e2) inter

consider e being Event of DS such that

O2: ( e = o & e1 < e & e < e2 & e in p,tr ) by O1;

thus o in (e1,e2) inter by O2; :: thesis: verum

for p being Process of DS

for tr being trace of DS

for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let DS be DistributedSysWithSharedMem of Values; :: thesis: for p being Process of DS

for tr being trace of DS

for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let p be Process of DS; :: thesis: for tr being trace of DS

for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let tr be trace of DS; :: thesis: for e1, e2 being Event of DS holds (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let e1, e2 be Event of DS; :: thesis: (e1,e2) interval_in (p,tr) c= (e1,e2) inter

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (e1,e2) interval_in (p,tr) or o in (e1,e2) inter )

assume O1: o in (e1,e2) interval_in (p,tr) ; :: thesis: o in (e1,e2) inter

consider e being Event of DS such that

O2: ( e = o & e1 < e & e < e2 & e in p,tr ) by O1;

thus o in (e1,e2) inter by O2; :: thesis: verum