Class (EqRelOf A) = {} ;
hence QuotientOrder A is empty by Def7; :: thesis: verum