let A be ext-real-membered set ; :: thesis: A c= [.(inf A),(sup A).]
let x be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not x in A or x in [.(inf A),(sup A).] )
assume A1: x in A ; :: thesis: x in [.(inf A),(sup A).]
then A2: x <= sup A by Th4;
inf A <= x by A1, Th3;
hence x in [.(inf A),(sup A).] by A2, XXREAL_1:1; :: thesis: verum