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.[ )
per cases ( A is empty or not A is empty ) ;
suppose A1: A is empty ; :: thesis: ex r, s being ExtReal st
( 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;
suppose A2: not A is empty ; :: thesis: ex r, s being ExtReal st
( 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;
end;