let A be Preorder; :: thesis: the carrier of (QuotientOrder A) is a_partition of the carrier of A
the carrier of (QuotientOrder A) = Class (EqRelOf A) by Def7;
hence the carrier of (QuotientOrder A) is a_partition of the carrier of A ; :: thesis: verum