for L being Lattice holds
( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )