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₁[ ExtReal] means ( $1 in A & $1 < x );
defpred S₂[ 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 )

proof

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;

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

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

suppose for r being ExtReal holds not S₁[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;

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 A5, XXREAL_1:4; :: thesis: verum

end;

suppose that A6: ex r being ExtReal st S₁[r] and
A7: ex r being ExtReal st S₂[r] ; :: thesis: x in A

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;

end;