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

proof

given x being object such that A1: x in [.+infty,p.[ ; :: thesis: contradiction
reconsider s = x as ExtReal by A1;
A2: +infty <= s by A1, Th3;
s < p by A1, Th3;
then p > +infty by A2, XXREAL_0:2;
hence contradiction by XXREAL_0:3; :: thesis: verum

end;

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