EqRelOf D is_symmetric_in field (EqRelOf D)
by RELAT_2:def 11;

then the InternalRel of (PreorderFromPartition D) is_symmetric_in the carrier of (PreorderFromPartition D) by ORDERS_1:12;

hence PreorderFromPartition D is symmetric by NECKLACE:def 3; :: thesis: verum

then the InternalRel of (PreorderFromPartition D) is_symmetric_in the carrier of (PreorderFromPartition D) by ORDERS_1:12;

hence PreorderFromPartition D is symmetric by NECKLACE:def 3; :: thesis: verum