ERl D is_symmetric_in field (ERl 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