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