dom (F .. A) = I by PBOOLE:def 3;
hence F .. A is ManySortedSet of I ; :: thesis: verum