theorem Th5: :: CONLAT_1:5

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