let A be ext-real-membered non left_end non right_end interval set ; :: thesis: ex r, s being ExtReal st

( r <= s & A = ].r,s.[ )

( r <= s & A = ].r,s.[ )

per cases
( A is empty or not A is empty )
;

end;

suppose A1:
A is empty
; :: thesis: ex r, s being ExtReal st

( r <= s & A = ].r,s.[ )

( r <= s & A = ].r,s.[ )

take
-infty
; :: thesis: ex s being ExtReal st

( -infty <= s & A = ].-infty,s.[ )

take -infty ; :: thesis: ( -infty <= -infty & A = ].-infty,-infty.[ )

thus ( -infty <= -infty & A = ].-infty,-infty.[ ) by A1; :: thesis: verum

end;( -infty <= s & A = ].-infty,s.[ )

take -infty ; :: thesis: ( -infty <= -infty & A = ].-infty,-infty.[ )

thus ( -infty <= -infty & A = ].-infty,-infty.[ ) by A1; :: thesis: verum

suppose A2:
not A is empty
; :: thesis: ex r, s being ExtReal st

( r <= s & A = ].r,s.[ )

( r <= s & A = ].r,s.[ )

take
inf A
; :: thesis: ex s being ExtReal st

( inf A <= s & A = ].(inf A),s.[ )

take sup A ; :: thesis: ( inf A <= sup A & A = ].(inf A),(sup A).[ )

thus inf A <= sup A by A2, Th40; :: thesis: A = ].(inf A),(sup A).[

thus A = ].(inf A),(sup A).[ by A2, Th78; :: thesis: verum

end;( inf A <= s & A = ].(inf A),s.[ )

take sup A ; :: thesis: ( inf A <= sup A & A = ].(inf A),(sup A).[ )

thus inf A <= sup A by A2, Th40; :: thesis: A = ].(inf A),(sup A).[

thus A = ].(inf A),(sup A).[ by A2, Th78; :: thesis: verum