let X be Subset of REAL; :: thesis: ( X is bounded_above implies X c= left_closed_halfline (upper_bound X) )
assume A1: X is bounded_above ; :: thesis: X c= left_closed_halfline (upper_bound X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in left_closed_halfline (upper_bound X) )
assume A2: x in X ; :: thesis: x in left_closed_halfline (upper_bound X)
then reconsider x = x as Real ;
x <= upper_bound X by A1, A2, SEQ_4:def 1;
hence x in left_closed_halfline (upper_bound X) by XXREAL_1:234; :: thesis: verum