let a, b, c be ExtReal; :: thesis: min ((min (a,b)),c) = min (a,(min (b,c)))

per cases
( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) )
by Th2;

end;

suppose
( a <= b & a <= c )
; :: thesis: min ((min (a,b)),c) = min (a,(min (b,c)))

then
( min (a,b) = a & min (a,c) = a )
by Def8;

hence min ((min (a,b)),c) = min (a,(min (b,c))) by Def8; :: thesis: verum

end;hence min ((min (a,b)),c) = min (a,(min (b,c))) by Def8; :: thesis: verum