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