let p be ExtReal; :: thesis: ].p,-infty.] = {}
for x being object holds not x in ].p,-infty.]

proof

given x being object such that A1: x in ].p,-infty.] ; :: thesis: contradiction
reconsider s = x as ExtReal 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.] = {} ; :: thesis: verum