Theorem Set.finite_of_forall_not_lt_lt

Modification history