defpred S_{1}[ Event of DS] means ( e1 < $1 & $1 < e2 & $1 in p,tr );

{ e where e is Event of DS : S_{1}[e] } c= the carrier of the events of DS

{ e where e is Event of DS : S

proof

hence
{ e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } is EventSet of DS
; :: thesis: verum
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { e where e is Event of DS : S_{1}[e] } or o in the carrier of the events of DS )

assume O1: o in { e where e is Event of DS : S_{1}[e] }
; :: thesis: o in the carrier of the events of DS

consider e being Event of DS such that

O2: ( e = o & S_{1}[e] )
by O1;

thus o in the carrier of the events of DS by O2; :: thesis: verum

end;assume O1: o in { e where e is Event of DS : S

consider e being Event of DS such that

O2: ( e = o & S

thus o in the carrier of the events of DS by O2; :: thesis: verum