theorem Th15: :: CONLAT_1:15

for C being FormalContext
for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)