[STATEMENT]
lemma desne_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) 
      dense_order_ow dense_order_ow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) dense_order_ow dense_order_ow
[PROOF STEP]
by 
    (
      ow_locale_transfer locale_defs: 
        dense_order_ow_def dense_order_ow_axioms_def
    )