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 13;

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

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 13;

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