let A be non empty Interval; :: thesis: for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let x be Real; :: thesis: ( 0 < x implies for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A1: 0 < x ; :: thesis: for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let B be non empty Interval; :: thesis: ( B = x ** A & A = ].(inf A),(sup A).[ implies ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A2: B = x ** A ; :: thesis: ( not A = ].(inf A),(sup A).[ or ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
( A = ].(inf A),(sup A).[ implies ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )

proof

assume A3: A = ].(inf A),(sup A).[ ; :: thesis: ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
A4: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t & B is open_interval )

proof

let s, t be Real; :: thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t & B is open_interval ) )
assume that
A5: s = inf A and
A6: t = sup A ; :: thesis: ( inf B = x * s & sup B = x * t & B is open_interval )
( inf B = x * s & sup B = x * t & B is open_interval )

proof

s <= t by A5, A6, XXREAL_2:40;
then A7: x * s <= x * t by A1, XREAL_1:64;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A8: d = x * s ;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A9: g = x * t ;
A10: ].d,g.[ c= x ** A

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,g.[ or q in x ** A )
assume A11: q in ].d,g.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A12: q1 = q ;
A13: q1 < g by A11, A12, MEASURE5:def 1;
A14: q / x in A

proof

reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
A16: q3 < sup A

proof

consider p, o being Real such that
A17: ( p = q1 & o = g ) and
p <= o by A9, A12, A13;
p / x < o / x by A1, A13, A17, XREAL_1:74;
hence q3 < sup A by A1, A6, A9, A12, A17, XCMPLX_1:89; :: thesis: verum

end;

( d < q1 & x * (q / x) = q ) by A1, A11, A12, MEASURE5:def 1, XCMPLX_1:87;
then inf A < q3 by A1, A5, A8, A12, XREAL_1:64;
hence q / x in A by A3, A16, MEASURE5:def 1; :: thesis: verum

end;

q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A14, MEMBER_1:193; :: thesis: verum

end;

x ** A c= ].d,g.[

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,g.[ )
assume A18: q in x ** A ; :: thesis: q in ].d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A19: z2 in A and
A20: q = x * z2 by A18, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
inf A <= z2 by A3, A19, MEASURE5:def 1;
then consider 1o, 1ra being Real such that
A21: ( 1o = inf A & 1ra = z2 ) and
1o <= 1ra by A5;
1o < 1ra by A3, A19, A21, MEASURE5:def 1;
then A22: x * 1o < x * 1ra by A1, XREAL_1:68;
z2 <= sup A by A3, A19, MEASURE5:def 1;
then consider 2o, 2r being Real such that
A23: ( 2o = z2 & 2r = sup A ) and
2o <= 2r by A6;
( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def 1;
then consider 2o1, 2r1 being R_eal such that
A24: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
2o < 2r by A3, A19, A23, MEASURE5:def 1;
then 2o1 < 2r1 by A1, A24, XREAL_1:68;
hence q in ].d,g.[ by A5, A6, A8, A9, A20, A21, A23, A22, A24, MEASURE5:def 1; :: thesis: verum

end;

then x ** A = ].d,g.[ by A10;
hence ( inf B = x * s & sup B = x * t & B is open_interval ) by A2, A8, A9, A7, MEASURE5:def 2, MEASURE6:8, MEASURE6:12; :: thesis: verum

end;

hence ( inf B = x * s & sup B = x * t & B is open_interval ) ; :: thesis: verum

end;

A is open_interval by A3, MEASURE5:def 2;
then x ** A is open_interval by A1, Th7;
hence ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) by A2, A4, MEASURE6:16; :: thesis: verum

end;

hence ( not A = ].(inf A),(sup A).[ or ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) ) ; :: thesis: verum