dom J = I by PARTFUN1:def 4;
then J . i in rng J by FUNCT_1:def 5;
hence J . i is non empty Poset by Def5; :: thesis: verum