let A be ext-real-membered non left_end right_end connected set ; :: thesis: A = ].(inf A),(max A).]
let x be ext-real number ; :: 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 ) )
thus ( x in A implies x in ].(inf A),(max A).] ) :: thesis: ( not x in ].(inf A),(max A).] or x in A )

proof

assume Z: x in A ; :: thesis: x in ].(inf A),(max A).]
then A: ( inf A <= x & x <= max A ) by Th3, Th3B;
not inf A in A by Def5;
then inf A < x by A, Z, XXREAL_0:1;
hence x in ].(inf A),(max A).] by A, XXREAL_1:2; :: thesis: verum

end;

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

per cases ( for r being ext-real number holds not S₁[r] or 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:2; :: thesis: verum

end;

suppose ex r being ext-real number st S₁[r] ; :: thesis: x in A

then consider r being ext-real number such that
W3: r in A and
W4: r < x ;
B: max A in A by Def6;
x <= max A by Z, XXREAL_1:2;
then A: x in [.r,(max A).] by W4, XXREAL_1:1;
[.r,(max A).] c= A by W3, B, Def12;
hence x in A by A; :: thesis: verum

end;

end;