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