let C be FormalContext; :: thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . CP1,CP2 = (B-meet C) . CP2,CP1
let CP1, CP2 be strict FormalConcept of C; :: thesis: (B-meet C) . CP1,CP2 = (B-meet C) . CP2,CP1
( ex O being Subset of ex A being Subset of st
( (B-meet C) . CP1,CP2 = ConceptStr(# O,A #) & O = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP1 \/ the Intent of CP2)) ) & ex O' being Subset of ex A' being Subset of st
( (B-meet C) . CP2,CP1 = ConceptStr(# O',A' #) & O' = the Extent of CP2 /\ the Extent of CP1 & A' = (ObjectDerivation C) . ((AttributeDerivation C) . (the Intent of CP2 \/ the Intent of CP1)) ) ) by Def21;
hence (B-meet C) . CP1,CP2 = (B-meet C) . CP2,CP1 ; :: thesis: verum