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

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