set qa = QuotientOrder A;
set car = the carrier of (QuotientOrder A);
set int = the InternalRel of (QuotientOrder A);
<=E A partially_orders Class (EqRel A) by DICKSON:9;
then the InternalRel of (QuotientOrder A) partially_orders Class (EqRel A) by Th44;
then the InternalRel of (QuotientOrder A) partially_orders Class (EqRelOf A) by Th41;
then the InternalRel of (QuotientOrder A) partially_orders the carrier of (QuotientOrder A) by Def7;
then ( QuotientOrder A is reflexive & QuotientOrder A is antisymmetric & QuotientOrder A is transitive ) by Th39;
hence ( QuotientOrder A is reflexive & QuotientOrder A is total & QuotientOrder A is antisymmetric & QuotientOrder A is transitive ) ; :: thesis: verum