a . i in rng a by Def3;
hence not a . i is empty by RELAT_1:def 9; :: thesis: verum