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 S_{1}[ 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 )

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 S

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 A4:
x in ].(inf A),(max A).]
; :: thesis: x in A
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 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

per cases
( for r being ExtReal holds not S_{1}[r] or ex r being ExtReal st S_{1}[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 A4, XXREAL_1:2; :: thesis: verum

end;then x <= inf A by Def4;

hence x in A by A4, XXREAL_1:2; :: thesis: verum