theorem Th17: :: CONLAT_1:17

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