Open: Inter_finite -> Inter.

Lebesgue/Set_theory/Set_system/Set_system_def_any.v

@@ -28,7 +28,7 @@ Inductive Open : set_system U :=
   | Open_Gen : Incl gen Open
   | Open_wEmpty : wEmpty Open
   | Open_wFull : wFull Open
-  | Open_Inter_finite : Inter_finite Open
+  | Open_Inter : Inter Open
   | Open_Unionf_any : Unionf_any Open.
 
 (* Closed is the collection of closed sets generated by gen,
@@ -37,7 +37,7 @@ Inductive Closed : set_system U :=
   | Closed_Gen : Incl gen Closed
   | Closed_wEmpty : wEmpty Closed
   | Closed_wFull : wFull Closed
-  | Closed_Union_finite : Union_finite Closed
+  | Closed_Union : Union Closed
   | Closed_Interf_any : Interf_any Closed.
 
 End Set_system_Def1.