:: deftheorem defines ConceptLattice CONLAT_1:def 20 :
for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);