Section Relations_1.
   Variable U : Type.

   Definition Relation := U → U → Prop.
   Variable R : Relation.

   Definition Reflexive : Prop := ∀ x : U, R x x.

   Definition Transitive : Prop := ∀ x y z : U, R x y → R y z → R x z.

   Definition Symmetric : Prop := ∀ x y : U, R x y → R y x.

   Definition Antisymmetric : Prop :=
     ∀ x y : U, R x y → R y x → x = y :>U.

   Definition contains (R R' : Relation) : Prop :=
     ∀ x y : U, R' x y → R x y.

   Definition same_relation (R R' : Relation) : Prop :=
     contains R R' ∧ contains R' R.

   Inductive Preorder : Prop :=
       Definition_of_preorder : Reflexive → Transitive → Preorder.

   Inductive Order : Prop :=
       Definition_of_order :
         Reflexive → Transitive → Antisymmetric → Order.

   Inductive Equivalence : Prop :=
       Definition_of_equivalence :
         Reflexive → Transitive → Symmetric → Equivalence.

   Inductive PER : Prop :=
       Definition_of_PER : Symmetric → Transitive → PER.

End Relations_1.
Hint Unfold Reflexive.
Hint Unfold Transitive.
Hint Unfold Antisymmetric.
Hint Unfold Symmetric.
Hint Unfold contains.
Hint Unfold same_relation.
Hint Resolve Definition_of_preorder.
Hint Resolve Definition_of_order.
Hint Resolve Definition_of_equivalence.
Hint Resolve Definition_of_PER.