now

assume {} in rng (B --> c) ; :: thesis: contradiction
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

hence B --> c is non-empty by RELAT_1:def 9; :: thesis: verum