- [ apply (λr:U ⇒_\r1 V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
- exT ? (λy:V.x ♮r y ∧ y ∈ S) });
- intros; simplify; split; intro; cases e1; exists [1,3: apply w]
- [ apply (. (e ^ -1‡#)‡#); assumption
- | apply (. (e‡#)‡#); assumption]
- | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
- [ apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
- apply (if ?? (e ??)); assumption
- | apply (. #‡(#‡e1)); cases x; split; try assumption;
- apply (if ?? (e ^ -1 ??)); assumption]]
+ [ intro r; constructor 1;
+ [ apply (λS: Ω^V. {x | ∃y:V. x ♮r y ∧ y ∈ S }).
+ intros; simplify; split; intros; cases e1; cases x; exists; [1,3: apply w]
+ split; try assumption; [ apply (. (e^-1‡#)); | apply (. (e‡#));] assumption;
+ | intros; simplify; split; simplify; intros; cases e1; cases x;
+ exists [1,3: apply w] split; try assumption;
+ [ apply (. (#‡e^-1)); | apply (. (#‡e));] assumption]
+ | intros; intro; simplify; split; simplify; intros; cases e1; exists [1,3: apply w]
+ cases x; split; try assumption;
+ [ apply (. e^-1 a2 w); | apply (. e a2 w)] assumption;]