for C being FormalContext
for CP1, CP2 being Element of (ConceptLattice C) holds
( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )