proposition: Theorem Rstar_contains_Rplus : forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R).
proof: Proof. intros U R; red. intros x y H'; elim H'. - generalize Rstar_contains_R; intro T; red in T; auto with sets. - intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2