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