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