not {} in rng (B --> c) by TARSKI:def 1;
hence B --> c is non-empty by RELAT_1:def 9; :: thesis: verum