theorem Th3: :: CONLAT_1:3

for C being FormalContext
for O1, O2 being Subset of the carrier of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1