proposition: Lemma Exercise6_29b r: Noetherian_set r emptyset.
proof: Proof. split; fprops. move => X xns [w wx]; move: (xns _ wx). have ->: (induced_order r emptyset) = emptyset. by apply /set0_P => y /setI2_P [_]/setX_P [_ /in_set0]. by rewrite /substrate domain_set0 range_set0 setU2_id => /in_set0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)