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
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: ( (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)) ) by Def21;
(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;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A2: ( (B-join C) . CP',CP2 = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP' \/ the Extent of CP2)) & A' = the Intent of CP' /\ the Intent of CP2 ) by Def22;
A3: (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 Th16;
A4: the Extent of CP1 /\ the Extent of CP2 c= the Extent of CP2 by XBOOLE_1:17;
then A5: (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 A3, Th3, XBOOLE_1:28
.= (AttributeDerivation C) . the Intent of CP2 by Def13
.= the Extent of CP2 by Def13 ;
((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 Th17
.= ((ObjectDerivation C) . (the Extent of CP1 /\ ((AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2 by Def13
.= ((ObjectDerivation C) . (the Extent of CP1 /\ the Extent of CP2)) /\ the Intent of CP2 by Def13
.= ((ObjectDerivation C) . (the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2) by Def13
.= (ObjectDerivation C) . the Extent of CP2 by A4, Th3, XBOOLE_1:28
.= the Intent of CP2 by Def13 ;
hence (B-join C) . ((B-meet C) . CP1,CP2),CP2 = CP2 by A1, A2, A5; :: thesis: verum