:: deftheorem Def8 defines .: CONLAT_2:def 8 :
for C being FormalContext
for CP being ConceptStr over C
for b₃ being strict ConceptStr over C .: holds
( b₃ = CP .: iff ( the Extent of b₃ = the Intent of CP & the Intent of b₃ = the Extent of CP ) );