proposition: Lemma lub_sig_ok R : is_lub le_sig (lub_sig R) R.
proof: Proof. destruct (lub_ok (pr R)) as [h1 h2]. split. intros [x Px] Rx. unfold le_sig, Rof, lub_sig. simpl. apply h1. ex Px. hyp. intros x x_inf. unfold le_sig, Rof, lub_sig. simpl. apply h2. intros y [Py Ry]. apply (x_inf (exist Py)). hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SetUtil) Coq(Morphisms Basics)