proposition: Lemma Iincl_lim : forall J (I:natO-m>IUord), (forall n, Iincl J (I n)) -> Iincl J (Ilim I).
proof: Proof. unfold Ilim,Iincl; simpl; split. apply lub_le with (f:=Low @ I); intro. case (H n); auto. apply le_glb with (f:=Up @ I); intro. case (H n); auto. Qed.
imports: ALEA(Utheory)