let x, y be ExtReal; :: thesis: ( x < y implies [.x,y.[ is left_end )
assume A1: x < y ; :: thesis: [.x,y.[ is left_end
then x in [.x,y.[ by XXREAL_1:3;
hence inf [.x,y.[ in [.x,y.[ by A1, Th26; :: according to XXREAL_2:def 5 :: thesis: verum