let x, y be ExtReal; :: thesis: min {x,y} = min (x,y)

now :: thesis: ( ( y <= x & min {x,y} = y ) or ( x < y & min {x,y} = x ) )

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