theorem :: CONLAT_2:7

for C being FormalContext
for D being non empty Subset of (ConceptLattice C) holds
( the Extent of ("\/" (D,C)) = (AttributeDerivation C) . ((ObjectDerivation C) . (union { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) & the Intent of ("\/" (D,C)) = meet { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )