Initial version of Conditionally_Complete_Lattice.thy is complete.