take chi C,C ; :: thesis: chi C,C is [.0 ,1.] -valued
thus rng (chi C,C) c= [.0 ,1.] by RELAT_1:def 19; :: according to RELAT_1:def 19 :: thesis: verum