let C be FormalContext; :: thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)
let CP1, CP2 be strict FormalConcept of C; :: thesis: (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)
( 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-join C) . (CP2,CP1) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP1)) & A9 = the Intent of CP2 /\ the Intent of CP1 ) ) by Def18;
hence (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1) ; :: thesis: verum