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

x in [.x,y.[ by A1, XXREAL_1:3;

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

end;x in [.x,y.[ by A1, XXREAL_1:3;

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

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