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 5; :: thesis: verum