assume not Carrier J is non-empty ; :: thesis: contradiction
then {} in rng (Carrier J) by RELAT_1:def 9;
then consider i being object such that
A1: ( i in dom (Carrier J) & (Carrier J) . i = {} ) by FUNCT_1:def 3;
reconsider i = i as set by TARSKI:1;
consider R being 1-sorted such that
A2: ( R = J . i & (Carrier J) . i = the carrier of R ) by A1, PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A1, A2, FUNCT_1:3;
then not R is empty by WAYBEL_3:def 7;
hence contradiction by A1, A2; :: thesis: verum