let x, y be ExtReal; :: thesis: ( x <= y implies ( [.x,y.] is left_end & [.x,y.] is right_end ) )
assume A1: x <= y ; :: thesis: ( [.x,y.] is left_end & [.x,y.] is right_end )
then x in [.x,y.] by XXREAL_1:1;
then inf [.x,y.] in [.x,y.] by A1, Th25;
hence [.x,y.] is left_end ; :: thesis: [.x,y.] is right_end
y in [.x,y.] by A1, XXREAL_1:1;
hence sup [.x,y.] in [.x,y.] by A1, Th29; :: according to XXREAL_2:def 6 :: thesis: verum