let C be FormalContext; :: thesis: for CP1, CP2, CP3 being strict FormalConcept of C holds (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3)
let CP1, CP2, CP3 be strict FormalConcept of C; :: thesis: (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3)
(B-join C) . (CP1,CP2) in rng (B-join C) by Lm3;
then reconsider CP = (B-join C) . (CP1,CP2) as strict FormalConcept of C by Th31;
A1: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-join C) . (CP,CP3) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ the Extent of CP3)) & A9 = the Intent of CP /\ the Intent of CP3 ) ) by Def18;
(B-join C) . (CP2,CP3) in rng (B-join C) by Lm3;
then reconsider CP9 = (B-join C) . (CP2,CP3) as strict FormalConcept of C by Th31;
A2: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . (CP2,CP3) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3)) & A = the Intent of CP2 /\ the Intent of CP3 ) & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-join C) . (CP1,CP9) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP9)) & A9 = the Intent of CP1 /\ the Intent of CP9 ) ) by Def18;
(AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3))))) = (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3))))) by Th15
.= (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3))) by Th7
.= (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ (((ObjectDerivation C) . the Extent of CP2) /\ ((ObjectDerivation C) . the Extent of CP3))) by Th15
.= (AttributeDerivation C) . ((((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP3)) by XBOOLE_1:16
.= (AttributeDerivation C) . (((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP3)) by Th15
.= (AttributeDerivation C) . (((ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)))) /\ ((ObjectDerivation C) . the Extent of CP3)) by Th7
.= (AttributeDerivation C) . ((ObjectDerivation C) . (((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) \/ the Extent of CP3)) by Th15 ;
hence (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; :: thesis: verum