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