let L be RelStr ; :: thesis: for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})
let X be Subset of L; :: thesis: chi (X, the carrier of L) is Function of L,(BoolePoset {{}})
the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
hence chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) ; :: thesis: verum