let Values be Values_with_Bool; 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; 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; 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; 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; (e1,e2) interval_in (p,tr) c= (e1,e2) inter
let o be object ; TARSKI:def 3 ( 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)
; 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; verum