:: deftheorem defines "/\" CONLAT_2:def 2 :
for C being FormalContext
for D being Subset of (ConceptLattice C) holds "/\" (D,C) = "/\" (D,(ConceptLattice C));