include "formal_topology/relations.ma".
include "formal_topology/o-algebra.ma".
-
+(*
definition POW': objs1 SET → OAlgebra.
intro A; constructor 1;
[ apply (Ω^A);
[ intros 2; change in f3 with (eq1 ? a1 a2); change with (a2 ∈ f* a);
apply (. f3^-1‡#); assumption;
| assumption ]]]
-qed.
\ No newline at end of file
+qed.
+*)