|2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
qed.
+(*
+
definition reverse_pordered_set: pordered_set → pordered_set.
intros (p); apply (mk_pordered_set (reverse_excedence p));
generalize in match (reverse_excedence p); intros (E); cases E (T f cRf cTf);
}.
*)
+*)
+
definition total_order_property : ∀E:excedence. Type ≝
λE:excedence. ∀a,b:E. a ≰ b → a < b.