proposition: Lemma exists_smallest_ordinal_with : forall (p:EP), (exists x:E, (is_ordinal x&p x)) -> exists o:E, is_smallest_ordinal_with p o.
proof: Proof. ir. util (lgs_smallest_with_property (f:=ID)(p:=p)). am. am. Qed.
imports: Arith transfinite