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

now

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

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

A2: for z being LowerBound of {x,y} holds z <= y by Lm6;
y is LowerBound of {x,y} by A1, Lm5;
hence min {x,y} = y by A2, Def4; :: thesis: verum

end;

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

A4: for z being LowerBound of {x,y} holds z <= x by Lm6;
x is LowerBound of {x,y} by A3, Lm5;
hence min {x,y} = x by A4, Def4; :: thesis: verum

end;

end;

end;

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