let v be set ; :: according to YELLOW_1:def 3 :: thesis: ( v in rng (X --> L) implies v is RelStr )
assume A1: v in rng (X --> L) ; :: thesis: v is RelStr
rng (X --> L) c= {L} by FUNCOP_1:13;
hence v is RelStr by A1, TARSKI:def 1; :: thesis: verum