let x, y be ext-real number ; :: 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 by Def5; :: 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