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 )

per cases ( not S is empty or S is empty ) ;

suppose not S is empty ; :: thesis: ( not W in rng (S --> T) or W is reflexive )

assume W in rng (S --> T) ; :: thesis: W is reflexive
then W in {T} ;
hence W is reflexive by TARSKI:def 1; :: thesis: verum

end;

suppose A2: S is empty ; :: 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 A2; :: thesis: verum

end;

end;