theorem Th7: :: CONLAT_1:7

for C being FormalContext
for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))