let A be ext-real-membered left_end non right_end interval set ; :: thesis: A = [.(min A),(sup A).[
let x be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not x in A or x in [.(min A),(sup A).[ ) & ( not x in [.(min A),(sup A).[ or x in A ) )
defpred S₁[ ExtReal] means ( $1 in A & $1 > x );
thus ( x in A implies x in [.(min A),(sup A).[ ) :: thesis: ( not x in [.(min A),(sup A).[ or x in A )

proof

A1: not sup A in A by Def6;
assume A2: x in A ; :: thesis: x in [.(min A),(sup A).[
then A3: min A <= x by Th3;
x <= sup A by A2, Th4;
then x < sup A by A2, A1, XXREAL_0:1;
hence x in [.(min A),(sup A).[ by A3, XXREAL_1:3; :: thesis: verum

end;

assume A4: x in [.(min A),(sup A).[ ; :: thesis: x in A

per cases ( for r being ExtReal holds not S₁[r] or ex r being ExtReal st S₁[r] ) ;

suppose for r being ExtReal holds not S₁[r] ; :: thesis: x in A

then x is UpperBound of A by Def1;
then sup A <= x by Def3;
hence x in A by A4, XXREAL_1:3; :: thesis: verum

end;

suppose ex r being ExtReal st S₁[r] ; :: thesis: x in A

then consider r being ExtReal such that
A5: r in A and
A6: r > x ;
inf A <= x by A4, XXREAL_1:3;
then A7: x in [.(inf A),r.] by A6, XXREAL_1:1;
min A in A by Def5;
then [.(inf A),r.] c= A by A5, Def12;
hence x in A by A7; :: thesis: verum

end;

end;