A1: dom O = dom (O ~) by RELAT_2:12;
dom O = X by PARTFUN1:def 2;
hence O ~ is Order of X by A1, PARTFUN1:def 2; :: thesis: verum