let A be ext-real-membered left_end right_end interval set ; :: thesis: A = [.(min A),(max A).]

let x be ExtReal; :: 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 ) )

A1: max A in A by Def6;

thus ( x in A implies x in [.(min A),(max A).] ) :: thesis: ( not x in [.(min A),(max A).] or x in A )

then [.(min A),(max A).] c= A by A1, Def12;

hence ( not x in [.(min A),(max A).] or x in A ) ; :: thesis: verum

let x be ExtReal; :: 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 ) )

A1: max A in A by Def6;

thus ( x in A implies x in [.(min A),(max A).] ) :: thesis: ( not x in [.(min A),(max A).] or x in A )

proof

min A in A
by Def5;
assume A2:
x in A
; :: thesis: x in [.(min A),(max A).]

then A3: x <= max A by Th4;

min A <= x by A2, Th3;

hence x in [.(min A),(max A).] by A3, XXREAL_1:1; :: thesis: verum

end;then A3: x <= max A by Th4;

min A <= x by A2, Th3;

hence x in [.(min A),(max A).] by A3, XXREAL_1:1; :: thesis: verum

then [.(min A),(max A).] c= A by A1, Def12;

hence ( not x in [.(min A),(max A).] or x in A ) ; :: thesis: verum