let A be set ; :: thesis: for D being a_partition of A holds D = the carrier of (QuotientOrder (PreorderFromPartition D))
let D be a_partition of A; :: thesis: D = the carrier of (QuotientOrder (PreorderFromPartition D))
D = Class (EqRelOf (PreorderFromPartition D)) by Th50;
hence D = the carrier of (QuotientOrder (PreorderFromPartition D)) by Def7; :: thesis: verum