let A be bounded Subset of REAL ; :: thesis: A c= [.(inf A),(sup A).]
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in [.(inf A),(sup A).] )
assume A1: a in A ; :: thesis: a in [.(inf A),(sup A).]
then reconsider r = a as Real ;
A2: r <= sup A by A1, SEQ_4:def 4;
inf A <= r by A1, SEQ_4:def 5;
hence a in [.(inf A),(sup A).] by A2, XXREAL_1:1; :: thesis: verum