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