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

proof

given x being object such that A2: x in [.p,-infty.] ; :: thesis: contradiction
reconsider s = x as ExtReal by A2;
A3: p <= s by A2, Th1;
s <= -infty by A2, Th1;
hence contradiction by A1, A3, XXREAL_0:2, XXREAL_0:6; :: thesis: verum

end;

hence [.p,-infty.] = {} ; :: thesis: verum