theorem Th6: :: CONLAT_1:6

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