let p be ext-real number ; :: thesis: [.+infty ,p.[ = {}
for x being set holds not x in [.+infty ,p.[

proof

given x being set such that A1: x in [.+infty ,p.[ ; :: thesis: contradiction
reconsider s = x as ext-real number by A1;
( +infty <= s & s < p ) by A1, Th3;
then p > +infty by XXREAL_0:2;
hence contradiction by XXREAL_0:3; :: thesis: verum

end;

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