proposition: Theorem Rsym_imp_notRsym : forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Complement U R).
proof: Proof. unfold Symmetric, Complement. intros U R H' x y H'0; red; intro H'1; apply H'0; auto with sets. Qed.
imports: Relations_1