for L being complete Lattice
for C being FormalContext holds
( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex d being Function of the carrier' of C, the carrier of L st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) )