Do you want to get such an element, or to test that an element you have satisfies this property? I am asking because the second seems a sensible precondition to an operation. I don t know the B-Method specifically; I ve looked at some documents, but can t find a quick reference, so this may be wrong in some details.

The second should look like this (prj2 is used for the second projection):

HasGreatestTd(flight) = flight in flights and forall flight  (flight  in flights => prj2(flight) >= prj2(flight ))

Then the first is:

flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})

Forgive my ignorance, I m not familiar with the B-Method. But couldn t you use the uniqueness quantifier? It d look something like:

there exists a time td such that for all times td , td > td

and

for all td, td , td , if td > td and td > td then td == td

This, of course, assumes that there is exactly one element in the set. I can t really tell if the B-Method allows for the full power of first order logic but I assume you could come close to this.

It is possible to define functions in B. Functions have constant values and are to be listed in the ABSTRACT_CONSTANTS clause, and defined in the PROPERTIES clause. I try to explain how you can use this construct to solve your problem.

Follows a small excerpt where

1. a shortcut for the cartesian product giving flight information is introduced;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. four constants are declared, the first three are "accessors", and the last maps a non-empty set of flight informations to the flight information with the largest departure time.

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. Then these constants are typed and defined as total functions. Note that the last function must take as input a non-empty set. Here I used to different approaches to specify these functions. One is definitional (with an equality), and the other is axiomatic.

PROPERTIES
    // typing 
    flight_no: FLIGHT_INFO --> FLIGHT_NO &
    flight_departure: FLIGHT_INFO --> TIME &
    flight_arrival: FLIGHT_INFO --> TIME &
    last_flight : POW1(FLIGHT_INFO) --> FLIGHT_INFO &
    // value
    flight_no = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | no) &
    flight_departure = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | dt) &
    flight_arrival = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | at) &
    !fs.(fs : POW1(FLIGHT_INFO) =>
       last_flight(fs) : fs &
       !(fi).(fi : FLIGHT_INFO & fi : fs =>
          flight_departure(fi) <= flight_departure(last_flight(fs)))