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

proof

let z be LowerBound of [.x,y.]; :: thesis: z <= x
x in [.x,y.] by A1, XXREAL_1:1;
hence z <= x by Def2; :: thesis: verum

end;

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