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

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