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