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;

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;

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

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

end;

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

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

end;

end;