let C be FormalContext; :: thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C)
let CP1, CP2 be strict FormalConcept of C; :: thesis: (B-join C) . (CP1,CP2) in rng (B-join C)
( CP1 in B-carrier C & CP2 in B-carrier C ) by Th31;
then [CP1,CP2] in [:(B-carrier C),(B-carrier C):] by ZFMISC_1:def 2;
then [CP1,CP2] in dom (B-join C) by FUNCT_2:def 1;
hence (B-join C) . (CP1,CP2) in rng (B-join C) by FUNCT_1:def 3; :: thesis: verum