let A be ext-real-membered left_end right_end connected set ; :: thesis: A = [.(min A),(max A).]
let x be ext-real number ; :: according to MEMBERED:def 14 :: thesis: ( ( not x in A or x in [.(min A),(max A).] ) & ( not x in [.(min A),(max A).] or x in A ) )
thus ( x in A implies x in [.(min A),(max A).] ) :: thesis: ( not x in [.(min A),(max A).] or x in A )

proof

assume x in A ; :: thesis: x in [.(min A),(max A).]
then ( min A <= x & x <= max A ) by Th3, Th3B;
hence x in [.(min A),(max A).] by XXREAL_1:1; :: thesis: verum

end;

( min A in A & max A in A ) by Def5, Def6;
then [.(min A),(max A).] c= A by Def12;
hence ( not x in [.(min A),(max A).] or x in A ) ; :: thesis: verum