let a, b be ext-real number ; :: thesis: min a,b <= a
( a <= b or not a <= b ) ;
hence min a,b <= a by Def8; :: thesis: verum