let C be FormalContext; :: thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C
let CP be strict FormalConcept of C; :: thesis: (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: (B-meet C) . (CP,(Concept-with-all-Attributes C)) = ConceptStr(# O,A #) and
A2: O = the Extent of CP /\ the Extent of (Concept-with-all-Attributes C) and
A3: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Attributes C))) by Def21;
A4: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the carrier' of C)) by A3, Th24
.= (ObjectDerivation C) . ((AttributeDerivation C) . the carrier' of C) by XBOOLE_1:12
.= (ObjectDerivation C) . ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Th24
.= (ObjectDerivation C) . the Extent of (Concept-with-all-Attributes C) by Def13
.= the Intent of (Concept-with-all-Attributes C) by Def13 ;
O = ((AttributeDerivation C) . the Intent of CP) /\ the Extent of (Concept-with-all-Attributes C) by A2, Def13
.= ((AttributeDerivation C) . the Intent of CP) /\ ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Def13
.= (AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Attributes C)) by Th17
.= (AttributeDerivation C) . ( the Intent of CP \/ the carrier' of C) by Th24
.= (AttributeDerivation C) . the carrier' of C by XBOOLE_1:12
.= (AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C) by Th24
.= the Extent of (Concept-with-all-Attributes C) by Def13 ;
hence (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C by A1, A4; :: thesis: verum