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

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