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 Th18;
let z be LowerBound of ].x,y.]; :: thesis: z <= x

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

z <= r

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

z <= r

proof

hence
z <= x
by A1, XREAL_1:228; :: thesis: verum
let r be ExtReal; :: 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:2;

hence z <= r by Def2; :: thesis: verum

end;assume that

A3: x < r and

A4: r < y ; :: thesis: z <= r

r in ].x,y.] by A3, A4, XXREAL_1:2;

hence z <= r by Def2; :: thesis: verum

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