let C be FormalContext; :: thesis: ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic
DualHomomorphism C is bijective by Th21;
hence ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic by LATTICE4:def 3; :: thesis: verum