let C be FormalContext; 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; (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 CP9 = (B-join 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-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 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, Def18;
(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 Th16;
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 Def9
.=
the Intent of CP1
by Def9
;
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 Th15
.=
the Extent of CP1 /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ ((ObjectDerivation C) . the Extent of CP2)))
by Def9
.=
the Extent of CP1 /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2))
by Def9
.=
((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2))
by Def9
.=
(AttributeDerivation C) . the Intent of CP1
by A1, Th4, XBOOLE_1:28
.=
the Extent of CP1
by Def9
;
hence
(B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1
by A2, A3; verum