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

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