let x, y be ext-real number ; :: thesis: ( x < y implies [.x,y.[ is left_end )
assume Z: x < y ; :: thesis: [.x,y.[ is left_end
x in [.x,y.[ by Z, XXREAL_1:3;
hence inf [.x,y.[ in [.x,y.[ by Z, Th26; :: according to XXREAL_2:def 5 :: thesis: verum