assume [.r,s.[ is right_end ; :: thesis: contradiction
then A3: sup [.r,s.[ in [.r,s.[ ;
then A4: sup [.r,s.[ < s by XXREAL_1:3;
r <= sup [.r,s.[ by A3, XXREAL_1:3;
then r < s by A4, XXREAL_0:2;
then s = sup [.r,s.[ by Th31;
hence contradiction by A3, XXREAL_1:3; :: thesis: verum