let x, y be ext-real number ; :: thesis: ( x < y implies inf ].x,y.] = x )
A: x is LowerBound of ].x,y.] by Th18;
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
for r being ext-real number st x < r & r < y holds
z <= r

proof

let r be ext-real number ; :: thesis: ( x < r & r < y implies z <= r )
assume ( x < r & r < y ) ; :: thesis: z <= r
then r in ].x,y.] by XXREAL_1:2;
hence z <= r by Def2; :: thesis: verum

end;

hence z <= x by Z, XREAL_1:230; :: thesis: verum

end;

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