let p be ext-real number ; :: thesis: [.p,-infty .[ = {}
for x being set holds not x in [.p,-infty .[

proof

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

end;

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