theorem Th18: :: CONLAT_1:18

for C being FormalContext holds (AttributeDerivation C) . {} = the carrier of C