theorem Th2: :: CONLAT_2:2

for C being FormalContext
for D being non empty Subset-Family of the carrier of C holds (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }