fact noEventAtSameTime {
    all e1,e2: Event | (e1 != e2) and (e1.startDate.day + e1.endDate.day = e2.startDate.day + e2.endDate.day)
        implies
        (e1.endDate.time < e2.startDate.time or e2.endDate.time < e1.startDate.time)
}