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 ;
( inf A <= r & r <= sup A ) by A1, SEQ_4:def 4, SEQ_4:def 5;
hence a in [.(inf A),(sup A).] by XXREAL_1:1; :: thesis: verum