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 by A1, Th2;
hence contradiction by XXREAL_0:3; :: thesis: verum

end;

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