(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_basic_topology_of_o_basic_pair: BP → BTop.
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_basic_topology_of_o_basic_pair: BP → BTop.