let x, y be ext-real number ; :: thesis: min {x,y} = min x,y

now

per cases ( y <= x or x < y ) ;

case y <= x ; :: thesis: min {x,y} = y

then A: y is LowerBound of {x,y} by Lm3;
for z being LowerBound of {x,y} holds z <= y by Lm4;
hence min {x,y} = y by A, Def4; :: thesis: verum

end;

case x < y ; :: thesis: min {x,y} = x

then A: x is LowerBound of {x,y} by Lm3;
for z being LowerBound of {x,y} holds z <= x by Lm4;
hence min {x,y} = x by A, Def4; :: thesis: verum

end;

end;

end;

hence min {x,y} = min x,y by XXREAL_0:def 9; :: thesis: verum