thus not ].r,s.[ is left_end :: thesis: not ].r,s.[ is right_end
proof
assume ].r,s.[ is left_end ; :: thesis: contradiction
then A5: inf ].r,s.[ in ].r,s.[ ;
then A6: inf ].r,s.[ < s by XXREAL_1:4;
r < inf ].r,s.[ by A5, XXREAL_1:4;
then r < s by A6, XXREAL_0:2;
then r = inf ].r,s.[ by Th28;
hence contradiction by A5, XXREAL_1:4; :: thesis: verum
end;
assume ].r,s.[ is right_end ; :: thesis: contradiction
then A7: sup ].r,s.[ in ].r,s.[ ;
then A8: sup ].r,s.[ < s by XXREAL_1:4;
r < sup ].r,s.[ by A7, XXREAL_1:4;
then r < s by A8, XXREAL_0:2;
then s = sup ].r,s.[ by Th32;
hence contradiction by A7, XXREAL_1:4; :: thesis: verum