ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
hence CP is Element of (ConceptLattice C) by CONLAT_1:35; :: thesis: verum