theorem Th4: :: CONLAT_1:4

for C being FormalContext
for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds
(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1