let p be ext-real number ; :: thesis: ( p <> +infty implies [.+infty,p.] = {} )
assume A1: p <> +infty ; :: thesis: [.+infty,p.] = {}
for x being set holds not x in [.+infty,p.]

proof

given x being set such that A2: x in [.+infty,p.] ; :: thesis: contradiction
reconsider s = x as ext-real number by A2;
A3: +infty <= s by A2, Th1;
s <= p by A2, Th1;
hence contradiction by A1, A3, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

end;

hence [.+infty,p.] = {} by XBOOLE_0:def 1; :: thesis: verum