let X be set ; :: thesis: ( id X quasi_orders X & id X partially_orders X )
field (id X) = X \/ (rng (id X))
.= X \/ X
.= X ;
hence ( id X quasi_orders X & id X partially_orders X ) by Th31, Th34; :: thesis: verum