let X be set ; :: thesis: ( id X quasi_orders X & id X partially_orders X )
A1: field (id X) = X \/ (rng (id X)) by RELAT_1:71
.= X \/ X by RELAT_1:71
.= X ;
A2: id X is being_partial-order by Th120;
id X is being_quasi-order by Th120;
hence ( id X quasi_orders X & id X partially_orders X ) by A1, A2, Th127, Th130; :: thesis: verum