0 in NAT ;
then rng F <> {} by FUNCT_2:6;
hence proj2 F is non empty Subset-Family of X by XBOOLE_1:1; :: thesis: verum