chore(order/conditionally_complete_lattice): drop an unneeded `nonempty` assumption (#10132)
chore(order/conditionally_complete_lattice): drop an unneeded `nonempty` assumption (#10132)






leanprover-community/mathlib,leanprover-community/mathlib