let A be set ; :: thesis: for D being a_partition of A holds D = Class (EqRelOf (PreorderFromPartition D))
let D be a_partition of A; :: thesis: D = Class (EqRelOf (PreorderFromPartition D))
ERl D = EqRelOf (PreorderFromPartition D) by Th49;
hence D = Class (EqRelOf (PreorderFromPartition D)) by Def5; :: thesis: verum