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