let x, y be ext-real number ; :: thesis: ( x < y implies ].x,y.] is right_end )
assume Z: x < y ; :: thesis: ].x,y.] is right_end
y in ].x,y.] by Z, XXREAL_1:2;
hence sup ].x,y.] in ].x,y.] by Z, Th30; :: according to XXREAL_2:def 6 :: thesis: verum