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 , A being Subset of 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 Def22;
A4: A = the Intent of CP /\ the carrier' of C by A3, Th24
.= the Intent of CP by XBOOLE_1:28 ;
the carrier' of C c= the carrier' of C ;
then reconsider A' = the carrier' of C as Subset of ;
A5: ((AttributeDerivation C) . the Intent of CP) \/ ((AttributeDerivation C) . A') = (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, Def13
.= (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP \/ ((AttributeDerivation C) . the carrier' of C))) by Th24
.= (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . the Intent of CP)) by A5, Def13
.= (AttributeDerivation C) . the Intent of CP by Th8
.= the Extent of CP by Def13 ;
hence (B-join C) . CP,(Concept-with-all-Attributes C) = CP by A1, A4; :: thesis: verum