now

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

end;

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