theorem Th31: :: WAYBEL_6:31

for L being RelStr
for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})