+definition minus_star_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^U ⇒_2 Ω^V).
+ intros; constructor 1; intros;
+ [ constructor 1;
+ [ apply (λS: Ω^U. {y | ∀x:U. x ♮c y → x ∈ S});
+ intros; simplify; split; intros; apply f;
+ [ apply (. #‡e); | apply (. #‡e ^ -1)] assumption;
+ | intros; split; intro; simplify; intros;
+ [ apply (. #‡e^-1);| apply (. #‡e); ] apply f; assumption;]
+ | intros; intro; simplify; split; simplify; intros; apply f;
+ [ apply (. (e x a2)); assumption | apply (. (e^-1 x a2)); assumption]]
+qed.
+
+(* the same as Rest for a basic pair *)
+definition star_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^V ⇒_2 Ω^U).
+ intros; constructor 1;
+ [ intro r; constructor 1;
+ [ apply (λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S});
+ intros; simplify; split; intros; apply f;
+ [ apply (. e ‡#);| apply (. e^ -1‡#);] assumption;
+ | intros; split; simplify; intros;
+ [ apply (. #‡e^-1);| apply (. #‡e); ] apply f; assumption;]
+ | intros; intro; simplify; split; simplify; intros; apply f;
+ [ apply (. e a2 y); | apply (. e^-1 a2 y)] assumption;]
+qed.
+
+(* the same as Ext for a basic pair *)
+definition minus_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^V ⇒_2 Ω^U).