let C be FormalContext; :: thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2
let CP1, CP2 be strict FormalConcept of C; :: thesis: (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2
A1: the Extent of CP1 /\ the Extent of CP2 c= the Extent of CP2 by XBOOLE_1:17;
(B-meet C) . (CP1,CP2) in rng (B-meet C) by Lm2;
then reconsider CP9 = (B-meet C) . (CP1,CP2) 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) . (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-join C) . (CP9,CP2) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP9 \/ the Extent of CP2)) & A9 = the Intent of CP9 /\ the Intent of CP2 ) ) by Def17, Def18;
(AttributeDerivation C) . ((ObjectDerivation C) . (( the Extent of CP1 /\ the Extent of CP2) \/ the Extent of CP2)) = (AttributeDerivation C) . (((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2)) by Th15;
then A3: (AttributeDerivation C) . ((ObjectDerivation C) . (( the Extent of CP1 /\ the Extent of CP2) \/ the Extent of CP2)) = (AttributeDerivation C) . ((ObjectDerivation C) . the Extent of CP2) by A1, Th3, XBOOLE_1:28
.= (AttributeDerivation C) . the Intent of CP2 by Def9
.= the Extent of CP2 by Def9 ;
((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) /\ the Intent of CP2 = ((ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2 by Th16
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ ((AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2 by Def9
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ the Intent of CP2 by Def9
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2) by Def9
.= (ObjectDerivation C) . the Extent of CP2 by A1, Th3, XBOOLE_1:28
.= the Intent of CP2 by Def9 ;
hence (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2 by A2, A3; :: thesis: verum