let f be PartFunc of REAL ,REAL ; :: thesis:
let A, B, C be closed-interval Subset of REAL ; :: thesis:
let X be set ; :: thesis:
assume that
A1: A c= X and
A2: f is_differentiable_on X and
A3: (f `| X) | A is continuous and
A4: inf A = inf B and
A5: sup B = inf C and
A6: sup C = sup A ; :: thesis:
X: A c= dom (f `| X) by A2, A1, FDIFF_1:def 8;
consider x being Real such that
A7: x in B by SUBSET_1:10;
( inf B <= x & x <= sup B ) by A7, INTEGRA2:1;
then A8: inf B <= sup B by XXREAL_0:2;
consider x being Real such that
A9: x in C by SUBSET_1:10;
( inf C <= x & x <= sup C ) by A9, INTEGRA2:1;
then A10: inf C <= sup C by XXREAL_0:2;
for x being set st x in B holds
x in A

let x be set ; :: thesis:
assume A11: x in B ; :: thesis:
then reconsider x = x as Real ;
( inf B <= x & x <= sup B ) by A11, INTEGRA2:1;
then ( inf A <= x & x <= sup A ) by A4, A5, A6, A10, XXREAL_0:2;
hence x in A by INTEGRA2:1; :: thesis:

end;

hence A12: B c= A by TARSKI:def 3; :: thesis:
for x being set st x in C holds
x in A

let x be set ; :: thesis:
assume A13: x in C ; :: thesis:
then reconsider x = x as Real ;
( inf C <= x & x <= sup C ) by A13, INTEGRA2:1;
then ( inf A <= x & x <= sup A ) by A4, A5, A6, A8, XXREAL_0:2;
hence x in A by INTEGRA2:1; :: thesis:

end;