let x, y be ExtReal; :: thesis: ( x < y implies ].x,y.] is right_end )
assume A1: x < y ; :: thesis: ].x,y.] is right_end
then y in ].x,y.] by XXREAL_1:2;
hence sup ].x,y.] in ].x,y.] by A1, Th30; :: according to XXREAL_2:def 6 :: thesis: verum