{} is Element of bool the carrier of the non empty LinearPreorder by SUBSET_1:1;
then consider E0 being Element of bool the carrier of the non empty LinearPreorder such that
E0def: E0 = {} ;
deffunc H₁( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;
consider procE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that
procE0def: for p being Element of the non empty set holds procE0 . p = H₁(p) from FUNCT_2:sch 4();
deffunc H₂( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;
consider traceE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that
traceE0def: for tr being Element of the non empty set holds traceE0 . tr = H₂(tr) from FUNCT_2:sch 4();
deffunc H₃( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;
consider readE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that
readE0def: for x being Element of the non empty set holds readE0 . x = H₃(x) from FUNCT_2:sch 4();
deffunc H₄( Element of the non empty set ) -> Element of bool the carrier of the non empty LinearPreorder = E0;
consider writeE0 being Function of the non empty set ,(bool the carrier of the non empty LinearPreorder) such that
writeE0def: for x being Element of the non empty set holds writeE0 . x = H₄(x) from FUNCT_2:sch 4();
take Se = Events_structure(# the non empty LinearPreorder, the non empty set , the non empty set , the non empty set ,procE0,traceE0,readE0,writeE0, the PartFunc of the carrier of the non empty LinearPreorder, the carrier of Values #); :: thesis:
C1: Se is pr-complete

proof

let tr be trace of Se; :: according to PETERSON:def 13 :: thesis:
let e be Event of Se; :: thesis:
assume U1: e in tr ; :: thesis:
take the Process of Se ; :: thesis:
thus e in the Process of Se by U1, E0def, traceE0def; :: thesis:

end;

C2: Se is pr-ordered

proof

let p be Process of Se; :: according to PETERSON:def 14 :: thesis:
let e1, e2 be Event of Se; :: thesis:
assume U1: ( e1 in p & e2 in p ) ; :: thesis:
thus ( not e1 <= e2 or not e2 <= e1 or e1 = e2 ) by U1, E0def, procE0def; :: thesis:

end;

C3: Se is rw-ordered

proof

let x be Location of Se; :: according to PETERSON:def 15 :: thesis:
let e1, e2 be Event of Se; :: thesis:
assume U1: ( ( e1 reads x or e1 writesto x ) & ( e2 reads x or e2 writesto x ) ) ; :: thesis:
thus ( not e1 <= e2 or not e2 <= e1 or e1 = e2 ) by U1, E0def, readE0def, writeE0def; :: thesis:

end;

C4: Se is rw-consistent

proof

let tr be trace of Se; :: according to PETERSON:def 16 :: thesis:
let x be Location of Se; :: thesis:
let e be Event of Se; :: thesis:
let a be Element of the carrier of Values; :: thesis:
assume U1: ( e in tr & e reads x & val e = a ) ; :: thesis:
thus ex e0 being Event of Se st
( e0 in tr & e0 < e & e0 writesto x & val e0 = a & ( for e1 being Event of Se st e1 in tr & e1 <= e & e1 writesto x holds
e1 <= e0 ) ) by U1, E0def, traceE0def; :: thesis:

end;

Se is rw-exclusive

proof

let e be Event of Se; :: according to PETERSON:def 17 :: thesis:
let x1, x2 be Location of Se; :: thesis:
thus ( not e reads x1 or not e writesto x2 ) by E0def, readE0def; :: thesis:

end;

hence Se is consistent by C1, C2, C3, C4; :: thesis: