let a, b be ExtReal; :: thesis: min (a,b) <= a
( a <= b or not a <= b ) ;
hence min (a,b) <= a by Def8; :: thesis: verum