dom X = [:I,J:]
by PARTFUN1:def 2;

then dom (~ X) = [:J,I:] by FUNCT_4:46;

hence ~ X is [:J,I:] -defined by RELAT_1:def 18; :: thesis: verum

then dom (~ X) = [:J,I:] by FUNCT_4:46;

hence ~ X is [:J,I:] -defined by RELAT_1:def 18; :: thesis: verum