let I be non empty closed_interval Subset of REAL; :: thesis: for c being Real st c in I holds
( [.(lower_bound I),c.] is non empty closed_interval Subset of REAL & [.c,(upper_bound I).] is non empty closed_interval Subset of REAL & upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).] )
let c be Real; :: thesis: ( c in I implies ( [.(lower_bound I),c.] is non empty closed_interval Subset of REAL & [.c,(upper_bound I).] is non empty closed_interval Subset of REAL & upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).] ) )
assume A1: c in I ; :: thesis: ( [.(lower_bound I),c.] is non empty closed_interval Subset of REAL & [.c,(upper_bound I).] is non empty closed_interval Subset of REAL & upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).] )
consider a, b being Real such that
A2: a <= b and
A3: I = [.a,b.] by Th33;
A4: ( lower_bound I = a & upper_bound I = b ) by A2, A3, JORDAN5A:19;
A5: ( a <= c & c <= b ) by A1, A3, XXREAL_1:1;
hence ( [.(lower_bound I),c.] is non empty closed_interval Subset of REAL & [.c,(upper_bound I).] is non empty closed_interval Subset of REAL ) by A4, XXREAL_1:30, MEASURE5:def 3; :: thesis: upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).]
upper_bound [.(lower_bound I),c.] = c by A4, A5, JORDAN5A:19;
hence upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).] by A4, A5, JORDAN5A:19; :: thesis: verum