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 )
( (B-meet C) . CP1,CP2 in rng (B-meet C) & (B-join C) . CP1,CP2 in rng (B-join C) ) by Lm2, Lm3;
hence ( (B-meet C) . CP1,CP2 is strict FormalConcept of C & (B-join C) . CP1,CP2 is strict FormalConcept of C ) by Th35; :: thesis: verum