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