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