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

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