let x, y be ext-real number ; :: thesis: ( x <= y implies ( [.x,y.] is left_end & [.x,y.] is right_end ) )
assume Z: x <= y ; :: thesis: ( [.x,y.] is left_end & [.x,y.] is right_end )
thus [.x,y.] is left_end :: thesis: [.x,y.] is right_end

proof

x in [.x,y.] by Z, XXREAL_1:1;
hence inf [.x,y.] in [.x,y.] by Z, Th25; :: according to XXREAL_2:def 5 :: thesis: verum

end;

y in [.x,y.] by Z, XXREAL_1:1;
hence sup [.x,y.] in [.x,y.] by Z, Th29; :: according to XXREAL_2:def 6 :: thesis: verum