let C be FormalContext; :: thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP
let CP be strict FormalConcept of C; :: thesis: (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: (B-meet C) . (CP,(Concept-with-all-Objects C)) = ConceptStr(# O,A #) and
A2: O = the Extent of CP /\ the Extent of (Concept-with-all-Objects C) and
A3: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Objects C))) by Def17;
A4: O = the Extent of CP /\ the carrier of C by A2, Th23
.= the Extent of CP by XBOOLE_1:28 ;
the carrier of C c= the carrier of C ;
then reconsider O9 = the carrier of C as Subset of the carrier of C ;
A5: ((ObjectDerivation C) . the Extent of CP) \/ ((ObjectDerivation C) . O9) = (ObjectDerivation C) . the Extent of CP by Th3, XBOOLE_1:12;
A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ ((ObjectDerivation C) . the Extent of (Concept-with-all-Objects C)))) by A3, Def9
.= (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ ((ObjectDerivation C) . the carrier of C))) by Th23
.= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . the Extent of CP)) by A5, Def9
.= (ObjectDerivation C) . the Extent of CP by Th7
.= the Intent of CP by Def9 ;
hence (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP by A1, A4; :: thesis: verum