dom J = I by PBOOLE:def 3;
then J . i in rng J by FUNCT_1:def 5;
hence J . i is non empty TopStruct by WAYBEL_3:def 7; :: thesis: verum