let A be ext-real-membered non empty non left_end non right_end interval set ; :: thesis: A = ].(inf A),(sup A).[

let x be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not x in A or x in ].(inf A),(sup A).[ ) & ( not x in ].(inf A),(sup A).[ or x in A ) )

defpred S_{1}[ ExtReal] means ( $1 in A & $1 < x );

defpred S_{2}[ ExtReal] means ( $1 in A & $1 > x );

thus ( x in A implies x in ].(inf A),(sup A).[ ) :: thesis: ( not x in ].(inf A),(sup A).[ or x in A )

let x be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not x in A or x in ].(inf A),(sup A).[ ) & ( not x in ].(inf A),(sup A).[ or x in A ) )

defpred S

defpred S

thus ( x in A implies x in ].(inf A),(sup A).[ ) :: thesis: ( not x in ].(inf A),(sup A).[ or x in A )

proof

assume A5:
x in ].(inf A),(sup A).[
; :: thesis: x in A
assume A1:
x in A
; :: thesis: x in ].(inf A),(sup A).[

then A2: x <> sup A by Def6;

x <= sup A by A1, Th4;

then A3: x < sup A by A2, XXREAL_0:1;

A4: x <> inf A by A1, Def5;

inf A <= x by A1, Th3;

then inf A < x by A4, XXREAL_0:1;

hence x in ].(inf A),(sup A).[ by A3, XXREAL_1:4; :: thesis: verum

end;then A2: x <> sup A by Def6;

x <= sup A by A1, Th4;

then A3: x < sup A by A2, XXREAL_0:1;

A4: x <> inf A by A1, Def5;

inf A <= x by A1, Th3;

then inf A < x by A4, XXREAL_0:1;

hence x in ].(inf A),(sup A).[ by A3, XXREAL_1:4; :: thesis: verum

per cases
( for r being ExtReal holds not S_{1}[r] or for r being ExtReal holds not S_{2}[r] or ( ex r being ExtReal st S_{1}[r] & ex r being ExtReal st S_{2}[r] ) )
;

end;

suppose
for r being ExtReal holds not S_{1}[r]
; :: thesis: x in A

then
x is LowerBound of A
by Def2;

then x <= inf A by Def4;

hence x in A by A5, XXREAL_1:4; :: thesis: verum

end;then x <= inf A by Def4;

hence x in A by A5, XXREAL_1:4; :: thesis: verum

suppose
for r being ExtReal holds not S_{2}[r]
; :: thesis: x in A

then
x is UpperBound of A
by Def1;

then sup A <= x by Def3;

hence x in A by A5, XXREAL_1:4; :: thesis: verum

end;then sup A <= x by Def3;

hence x in A by A5, XXREAL_1:4; :: thesis: verum

suppose that A6:
ex r being ExtReal st S_{1}[r]
and

A7: ex r being ExtReal st S_{2}[r]
; :: thesis: x in A

A7: ex r being ExtReal st S

consider r being ExtReal such that

A8: r in A and

A9: r < x by A6;

consider s being ExtReal such that

A10: s in A and

A11: s > x by A7;

A12: x in [.r,s.] by A9, A11, XXREAL_1:1;

[.r,s.] c= A by A8, A10, Def12;

hence x in A by A12; :: thesis: verum

end;A8: r in A and

A9: r < x by A6;

consider s being ExtReal such that

A10: s in A and

A11: s > x by A7;

A12: x in [.r,s.] by A9, A11, XXREAL_1:1;

[.r,s.] c= A by A8, A10, Def12;

hence x in A by A12; :: thesis: verum