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