theorem :: CONLAT_1:11

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