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, Th2;
then p < -infty by XXREAL_0:2;
hence contradiction by XXREAL_0:5; :: thesis: verum

end;

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