let A be ext-real-membered non left_end right_end interval set ; :: thesis: A = ].(inf A),(max A).]
let x be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not x in A or x in ].(inf A),(max A).] ) & ( not x in ].(inf A),(max A).] or x in A ) )
defpred S1[ ExtReal] means ( $1 in A & $1 < x );
thus ( x in A implies x in ].(inf A),(max A).] ) :: thesis: ( not x in ].(inf A),(max A).] or x in A )
proof
A1: not inf A in A by Def5;
assume A2: x in A ; :: thesis: x in ].(inf A),(max A).]
then A3: x <= max A by Th4;
inf A <= x by A2, Th3;
then inf A < x by A2, A1, XXREAL_0:1;
hence x in ].(inf A),(max A).] by A3, XXREAL_1:2; :: thesis: verum
end;
assume A4: x in ].(inf A),(max A).] ; :: thesis: x in A
per cases ( for r being ExtReal holds not S1[r] or ex r being ExtReal st S1[r] ) ;
suppose for r being ExtReal holds not S1[r] ; :: thesis: x in A
then x is LowerBound of A by Def2;
then x <= inf A by Def4;
hence x in A by A4, XXREAL_1:2; :: thesis: verum
end;
suppose ex r being ExtReal st S1[r] ; :: thesis: x in A
then consider r being ExtReal such that
A5: r in A and
A6: r < x ;
x <= max A by A4, XXREAL_1:2;
then A7: x in [.r,(max A).] by A6, XXREAL_1:1;
max A in A by Def6;
then [.r,(max A).] c= A by A5, Def12;
hence x in A by A7; :: thesis: verum
end;
end;