let x, y be ExtReal; ( x <= y implies ( [.x,y.] is left_end & [.x,y.] is right_end ) )
assume A1:
x <= y
; ( [.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
; [.x,y.] is right_end
y in [.x,y.]
by A1, XXREAL_1:1;
hence
sup [.x,y.] in [.x,y.]
by A1, Th29; XXREAL_2:def 6 verum