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 Def21;
A4: O = the Extent of CP /\ the carrier of C by A2, Th24
.= 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, Def13
.= (ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP \/ ((ObjectDerivation C) . the carrier of C))) by Th24
.= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . the Extent of CP)) by A5, Def13
.= (ObjectDerivation C) . the Extent of CP by Th7
.= the Intent of CP by Def13 ;
hence (B-meet C) . CP,(Concept-with-all-Objects C) = CP by A1, A4; :: thesis: verum