let C be FormalContext; :: thesis: for CP1, CP2 being strict FormalConcept of C holds
( (B-meet C) . CP1,CP2 is strict FormalConcept of C & (B-join C) . CP1,CP2 is strict FormalConcept of C )
let CP1, CP2 be strict FormalConcept of C; :: thesis: ( (B-meet C) . CP1,CP2 is strict FormalConcept of C & (B-join C) . CP1,CP2 is strict FormalConcept of C )
A1: (B-meet C) . CP1,CP2 in rng (B-meet C) by Lm2;
(B-join C) . CP1,CP2 in rng (B-join C) by Lm3;
hence ( (B-meet C) . CP1,CP2 is strict FormalConcept of C & (B-join C) . CP1,CP2 is strict FormalConcept of C ) by A1, Th35; :: thesis: verum