theorem :: CONLAT_2:16

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