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:87, ZFMISC_1:30 ;
hence chi X,the carrier of L is Function of L,(BoolePoset {{} }) ; :: thesis: verum