let x, y be ExtReal; :: 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

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

assume A1: x < y ; :: thesis: inf ].x,y.[ = x

A2: for z being LowerBound of ].x,y.[ holds z <= x

proof

x is LowerBound of ].x,y.[
by Th20;
let z be LowerBound of ].x,y.[; :: thesis: z <= x

for r being ExtReal st x < r & r < y holds

z <= r by XXREAL_1:4, Def2;

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

end;for r being ExtReal st x < r & r < y holds

z <= r by XXREAL_1:4, Def2;

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

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