dom X = [:I,J:] by PBOOLE:def 3;
then dom (~ X) = [:J,I:] by FUNCT_4:47;
hence ~ X is ManySortedSet of [:J,I:] by PBOOLE:def 3; :: thesis: verum