theorem Th10: :: CONLAT_1:10

for C being FormalContext
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )