let C be FormalContext; :: thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . CP1,((B-join C) . CP1,CP2) = CP1
let CP1, CP2 be strict FormalConcept of C; :: thesis: (B-meet C) . CP1,((B-join C) . CP1,CP2) = CP1
A1: the Intent of CP1 /\ the Intent of CP2 c= the Intent of CP1 by XBOOLE_1:17;
(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 Th35;
A2: ( ex O being Subset of ex A being Subset of 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 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, Def22;
(ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP1 \/ (the Intent of CP1 /\ the Intent of CP2))) = (ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2))) by Th17;
then A3: (ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP1 \/ (the Intent of CP1 /\ the Intent of CP2))) = (ObjectDerivation C) . ((AttributeDerivation C) . the Intent of CP1) by A1, Th4, XBOOLE_1:28
.= (ObjectDerivation C) . the Extent of CP1 by Def13
.= the Intent of CP1 by Def13 ;
the Extent of CP1 /\ ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) = the Extent of CP1 /\ ((AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2))) by Th16
.= the Extent of CP1 /\ ((AttributeDerivation C) . (the Intent of CP1 /\ ((ObjectDerivation C) . the Extent of CP2))) by Def13
.= the Extent of CP1 /\ ((AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2)) by Def13
.= ((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2)) by Def13
.= (AttributeDerivation C) . the Intent of CP1 by A1, Th4, XBOOLE_1:28
.= the Extent of CP1 by Def13 ;
hence (B-meet C) . CP1,((B-join C) . CP1,CP2) = CP1 by A2, A3; :: thesis: verum