let A be ext-real-membered non empty non left_end non right_end connected set ; :: thesis: A = ].(inf A),(sup A).[
let x be ext-real number ; :: 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 ) )
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 Z: x in A ; :: thesis: x in ].(inf A),(sup A).[
then A: inf A <= x by Th3;
x <> inf A by Z, Def5;
then C: inf A < x by A, XXREAL_0:1;
B: x <= sup A by Z, Th3B;
x <> sup A by Z, Def6;
then x < sup A by B, XXREAL_0:1;
hence x in ].(inf A),(sup A).[ by C, XXREAL_1:4; :: thesis: verum

end;

assume Z: x in ].(inf A),(sup A).[ ; :: thesis: x in A
defpred S₁[ ext-real number ] means ( $1 in A & $1 < x );
defpred S₂[ ext-real number ] means ( $1 in A & $1 > x );

per cases ( for r being ext-real number holds not S₁[r] or for r being ext-real number holds not S₂[r] or ( ex r being ext-real number st S₁[r] & ex r being ext-real number st S₂[r] ) ) ;

suppose for r being ext-real number 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 Z, XXREAL_1:4; :: thesis: verum

end;

suppose for r being ext-real number 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 Z, XXREAL_1:4; :: thesis: verum

end;

suppose that S1: ex r being ext-real number st S₁[r] and
S2: ex r being ext-real number st S₂[r] ; :: thesis: x in A

consider r being ext-real number such that
W3: r in A and
W4: r < x by S1;
consider s being ext-real number such that
W5: s in A and
W6: s > x by S2;
A: x in [.r,s.] by W4, W6, XXREAL_1:1;
[.r,s.] c= A by W3, W5, Def12;
hence x in A by A; :: thesis: verum

end;

end;