consider j being Element of J;
Inf in rng (Infs ) by Th14;
hence not rng (Infs ) is empty ; :: thesis: verum