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 Def17;
A4: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the carrier' of C)) by A3, Th23
.= (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 Th23
.= (ObjectDerivation C) . the Extent of (Concept-with-all-Attributes C) by Def9
.= the Intent of (Concept-with-all-Attributes C) by Def9 ;
O = ((AttributeDerivation C) . the Intent of CP) /\ the Extent of (Concept-with-all-Attributes C) by A2, Def9
.= ((AttributeDerivation C) . the Intent of CP) /\ ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Def9
.= (AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Attributes C)) by Th16
.= (AttributeDerivation C) . ( the Intent of CP \/ the carrier' of C) by Th23
.= (AttributeDerivation C) . the carrier' of C by XBOOLE_1:12
.= (AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C) by Th23
.= the Extent of (Concept-with-all-Attributes C) by Def9 ;
hence (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C by A1, A4; :: thesis: verum