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

proof

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

end;

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