assume ].r,s.] is left_end ; :: thesis: contradiction
then A: inf ].r,s.] in ].r,s.] by Def5;
then ( r < inf ].r,s.] & inf ].r,s.] <= s ) by XXREAL_1:2;
then r < s by XXREAL_0:2;
then r = inf ].r,s.] by Th27;
hence contradiction by A, XXREAL_1:2; :: thesis: verum