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, RELAT_2:10, RELAT_2:23, RELAT_2:25; :: thesis: verum