let C be FormalContext; :: thesis: 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; :: thesis: (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 Th35;
reconsider CPa = (B-meet C) . CP,CP3 as strict FormalConcept of C by Lm4;
A1: ( ex O being Subset of ex A being Subset of 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 O' being Subset of ex A' being Subset of st
( (B-meet C) . CP,CP3 = ConceptStr(# O',A' #) & O' = the Extent of CP /\ the Extent of CP3 & A' = (ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP \/ the Intent of CP3)) ) ) by Def21;
(B-meet C) . CP2,CP3 in rng (B-meet C) by Lm2;
then reconsider CP' = (B-meet C) . CP2,CP3 as strict FormalConcept of C by Th35;
reconsider CPb = (B-meet C) . CP1,CP' as strict FormalConcept of C by Lm4;
A2: ( ex O being Subset of ex A being Subset of 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 O' being Subset of ex A' being Subset of st
( (B-meet C) . CP1,CP' = ConceptStr(# O',A' #) & O' = the Extent of CP1 /\ the Extent of CP' & A' = (ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP')) ) ) by Def21;
(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 Th17
.= (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 Th17
.= (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 Th17
.= (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 Th17 ;
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; :: thesis: verum