assume [.r,s.[ is right_end ; :: thesis: contradiction
then A: sup [.r,s.[ in [.r,s.[ by Def6;
then ( r <= sup [.r,s.[ & sup [.r,s.[ < s ) by XXREAL_1:3;
then r < s by XXREAL_0:2;
then s = sup [.r,s.[ by Th31;
hence contradiction by A, XXREAL_1:3; :: thesis: verum