defpred S1[ Event of DS] means ( e1 < $1 & $1 < e2 & $1 in p,tr );
{ e where e is Event of DS : S1[e] } c= the carrier of the events of DS
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { e where e is Event of DS : S1[e] } or o in the carrier of the events of DS )
assume O1: o in { e where e is Event of DS : S1[e] } ; :: thesis: o in the carrier of the events of DS
consider e being Event of DS such that
O2: ( e = o & S1[e] ) by O1;
thus o in the carrier of the events of DS by O2; :: thesis: verum
end;
hence { e where e is Event of DS : ( e1 < e & e < e2 & e in p,tr ) } is EventSet of DS ; :: thesis: verum