:: deftheorem defines .: CONLAT_2:def 7 :
for C being FormalContext holds C .: = ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);