proposition: Theorem Rsym_imp_Rstarsym : forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R).
proof: Proof. intros U R H'; red. intros x y H'0; elim H'0; auto with sets. intros x0 y0 z H'1 H'2 H'3. generalize Rstar_transitive; intro T1; red in T1. apply T1 with y0; auto with sets. apply Rstar_n with x0; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2