set f = S --> T;
let W be RelStr ; :: according to WAYBEL_3:def 8 :: thesis: ( not W in rng (S --> T) or W is reflexive )
assume W in rng (S --> T) ; :: thesis: W is reflexive
hence W is reflexive by TARSKI:def 1; :: thesis: verum