scheme :: INT_1:sch 6
IntMax{ F1() -> Integer, P1[ Integer] } :
ex i0 being Integer st
( P1[i0] & ( for i1 being Integer st P1[i1] holds
i1 <= i0 ) )
provided
A1: for i1 being Integer st P1[i1] holds
i1 <= F1() and
A2: ex i1 being Integer st P1[i1]