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 ) ) ) )
A3: inf A <= sup A by XXREAL_2:40;
assume A4: 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 ) ) )
then inf A <> sup A ;
then inf A < sup A by A3, XXREAL_0:1;
then sup A in A by A4, XXREAL_1:2;
then reconsider b = sup A as Real ;
A5: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t )

proof

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

proof

s <= t by A6, A7, XXREAL_2:40;
then A8: 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
A9: d = x * s ;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A10: g = x * t ;
A11: ].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 A12: q in ].d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A10;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A13: q / x in A

proof

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

proof

q1 <= g by A12, XXREAL_1:2;
then consider p, o being Real such that
A15: ( p = q1 & o = g ) and
A16: p <= o by A10;
p / x <= o / x by A1, A16, XREAL_1:72;
hence q3 <= sup A by A1, A7, A10, A15, XCMPLX_1:89; :: thesis: verum

end;

( d < q1 & x * (q / x) = q ) by A1, A12, XCMPLX_1:87, XXREAL_1:2;
then inf A < q3 by A1, A6, A9, XREAL_1:64;
hence q / x in A by A4, A14, XXREAL_1:2; :: thesis: verum

end;

q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A13, 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 A17: q in x ** A ; :: thesis: q in ].d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
reconsider q = q as R_eal by XXREAL_0:def 1;
inf A <= z2 by A4, A18, XXREAL_1:2;
then consider 1o, 1ra being Real such that
A20: ( 1o = inf A & 1ra = z2 ) and
1o <= 1ra by A6;
1o < 1ra by A4, A18, A20, XXREAL_1:2;
then A21: d < q by A1, A6, A9, A19, A20, XREAL_1:68;
z2 <= sup A by A4, A18, XXREAL_1:2;
then consider 2o, 2r being Real such that
A22: ( 2o = z2 & 2r = sup A ) and
A23: 2o <= 2r by A7;
x * 2o <= x * 2r by A1, A23, XREAL_1:64;
hence q in ].d,g.] by A7, A10, A19, A22, A21, XXREAL_1:2; :: thesis: verum

end;

then x ** A = ].d,g.] by A11;
hence ( inf B = x * s & sup B = x * t ) by A2, A9, A10, A8, MEASURE6:9, MEASURE6:13; :: thesis: verum

end;

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

end;

A = ].(inf A),b.] by A4;
then A is left_open_interval by MEASURE5:def 5;
then B is left_open_interval by A1, A2, Th11;
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 A5, MEASURE6:19; :: thesis: verum