A1: dom O = dom (O ~ ) by RELAT_2:29;
dom O = X by PARTFUN1:def 4;
hence O ~ is Order of X by A1, PARTFUN1:def 4, RELAT_2:27, RELAT_2:40, RELAT_2:42; :: thesis: verum