:: deftheorem defines Context CONLAT_2:def 6 :
for L being Lattice holds Context L = ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);