let C be FormalContext; :: thesis: ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C )
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: ( Concept-with-all-Objects C = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) ) by Def16;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A2: ( Concept-with-all-Attributes C = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} ) by Def17;
thus ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C ) by A1, A2, Th18, Th19; :: thesis: verum