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

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