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

proof

given x being object such that A2: x in [.+infty,p.] ; :: thesis: contradiction
reconsider s = x as ExtReal 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.] = {} ; :: thesis: verum