theorem Th23: :: CONLAT_1:23

for C being FormalContext holds
( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C )