assume ].r,s.] is left_end ; :: thesis: contradiction
then A1: inf ].r,s.] in ].r,s.] ;
then A2: inf ].r,s.] <= s by XXREAL_1:2;
r < inf ].r,s.] by A1, XXREAL_1:2;
then r < s by A2, XXREAL_0:2;
then r = inf ].r,s.] by Th27;
hence contradiction by A1, XXREAL_1:2; :: thesis: verum