theorem Th16: :: CONLAT_1:16

for C being FormalContext
for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)