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

end;

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