let a, b be ext-real number ; :: 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