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