let a, b, c be ext-real number ; :: 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 & ( min b,c = b or min b,c = c ) ) by Def8;
hence min (min a,b),c = min a,(min b,c) ; :: 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 & ( min a,b = a or min a,b = b ) ) by Def8;
hence min (min a,b),c = min a,(min b,c) ; :: thesis: verum

end;

end;