let C be FormalContext; for CP1, CP2, CP3 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)
let CP1, CP2, CP3 be strict FormalConcept of C; (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)
(B-meet C) . (CP1,CP2) in rng (B-meet C)
by Lm2;
then reconsider CP = (B-meet 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-meet C) . (CP1,CP2) = ConceptStr(# O,A #) & O = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( 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-meet C) . (CP,CP3) = ConceptStr(# O9,A9 #) & O9 = the Extent of CP /\ the Extent of CP3 & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the Intent of CP3)) ) )
by Def17;
(B-meet C) . (CP2,CP3) in rng (B-meet C)
by Lm2;
then reconsider CP9 = (B-meet 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-meet C) . (CP2,CP3) = ConceptStr(# O,A #) & O = the Extent of CP2 /\ the Extent of CP3 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( 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-meet C) . (CP1,CP9) = ConceptStr(# O9,A9 #) & O9 = the Extent of CP1 /\ the Extent of CP9 & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP9)) ) )
by Def17;
(ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3))))) =
(ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3)))))
by Th16
.=
(ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3)))
by Th8
.=
(ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ (((AttributeDerivation C) . the Intent of CP2) /\ ((AttributeDerivation C) . the Intent of CP3)))
by Th16
.=
(ObjectDerivation C) . ((((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . the Intent of CP2)) /\ ((AttributeDerivation C) . the Intent of CP3))
by XBOOLE_1:16
.=
(ObjectDerivation C) . (((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) /\ ((AttributeDerivation C) . the Intent of CP3))
by Th16
.=
(ObjectDerivation C) . (((AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)))) /\ ((AttributeDerivation C) . the Intent of CP3))
by Th8
.=
(ObjectDerivation C) . ((AttributeDerivation C) . (((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) \/ the Intent of CP3))
by Th16
;
hence
(B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)
by A1, A2, XBOOLE_1:16; verum