:: deftheorem defines is-SubConcept-of CONLAT_1:def 16 :
for C being FormalContext
for CP1, CP2 being FormalConcept of C holds
( CP1 is-SubConcept-of CP2 iff the Extent of CP1 c= the Extent of CP2 );