:: deftheorem Def18 defines B-join CONLAT_1:def 19 :
for C being FormalContext
for b₂ being BinOp of (B-carrier C) holds
( b₂ = B-join C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ . (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 ) );