let a, b be ExtReal; :: thesis: ( a <= min (a,b) implies min (a,b) = a )
assume min (a,b) >= a ; :: thesis: min (a,b) = a
then ( min (a,b) > a or min (a,b) = a ) by Th1;
hence min (a,b) = a by Th17; :: thesis: verum