let x, y be ext-real number ; :: thesis: ( x < y implies inf [.x,y.[ = x )
A: x is LowerBound of [.x,y.[ by Th19;
assume Z: x < y ; :: thesis: inf [.x,y.[ = x
for z being LowerBound of [.x,y.[ holds z <= x

proof

let z be LowerBound of [.x,y.[; :: thesis: z <= x
x in [.x,y.[ by Z, XXREAL_1:3;
hence z <= x by Def2; :: thesis: verum

end;

hence inf [.x,y.[ = x by A, Def4; :: thesis: verum