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;
s < -infty by A1, Th3;
hence contradiction by XXREAL_0:5; :: thesis: verum

end;

hence [.p,-infty.[ = {} ; :: thesis: verum