let x, y be ext-real number ; :: thesis: ( x < y implies inf ].x,y.[ = x )
assume A1: x < y ; :: thesis: inf ].x,y.[ = x
A2: 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 that
A3: x < r and
A4: r < y ; :: thesis: z <= r
r in ].x,y.[ by A3, A4, XXREAL_1:4;
hence z <= r by Def2; :: thesis: verum

end;

hence z <= x by A1, XREAL_1:228; :: thesis: verum

end;

x is LowerBound of ].x,y.[ by Th20;
hence inf ].x,y.[ = x by A2, Def4; :: thesis: verum