let X be set ; :: thesis: ( id X quasi_orders X & id X partially_orders X )
field (id X) = X \/ (rng (id X)) by RELAT_1:71
.= X \/ X by RELAT_1:71
.= X ;
hence ( id X quasi_orders X & id X partially_orders X ) by Th127, Th130; :: thesis: verum