- ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_inf (reverse_ordered_set O) a l → is_sup O a l.
- intros;
- apply mk_is_sup;
- [ apply reverse_is_lower_bound_is_upper_bound;
- change in l with (os_carrier (reverse_ordered_set O));
- apply (inf_lower_bound ? ? ? H)
- | intros;
- change in l with (os_carrier (reverse_ordered_set O));
- change in v with (os_carrier (reverse_ordered_set O));
- change with (os_le (reverse_ordered_set O) v l);
- apply (inf_greatest_lower_bound ? ? ? H);
- change in v with (os_carrier O);
- apply is_upper_bound_reverse_is_lower_bound;
- assumption
- ].
+ ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
+ is_inf (reverse_pordered_set O) a l → is_sup O a l.
+intros (O a l H); apply mk_is_sup;
+[1: apply reverse_is_lower_bound_is_upper_bound;
+ apply (inf_lower_bound (reverse_pordered_set O)); assumption
+|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v);
+ apply is_upper_bound_reverse_is_lower_bound; assumption;]