let C be FormalContext; :: thesis: for D being Subset of (ConceptLattice C) holds
( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )
let D be Subset of (ConceptLattice C); :: thesis: ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 20;
hence ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C ) by CONLAT_1:31; :: thesis: verum