[STATEMENT]
lemma le_of_comp_set_less_eq: 
  "le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le
[PROOF STEP]
by (rule le_of_comp_of_ords_gen, simp add: ord.set_less_def)