(**************************************************************************)
include "formal_topology/subsets.ma".
-
+(*
record binary_relation (A,B: SET) : Type[1] ≝
{ satisfy:> binary_morphism1 A B CPROP }.
definition full_subset: ∀s:REL. Ω^s.
- apply (λs.{x | ⊤});
+ apply (λs.{x | True});
intros; simplify; split; intro; assumption.
qed.
qed.
*)
+axiom daemon : False.
+
theorem extS_singleton:
∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x.
intros; unfold extS; unfold ext; unfold singleton; simplify;
split; intros 2; simplify; simplify in f;
[ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
| split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
+*)