let A be Interval; :: thesis: for x being real number holds
( A is left_open_interval iff x ++ A is left_open_interval )
let x be real number ; :: thesis: ( A is left_open_interval iff x ++ A is left_open_interval )
A1: for B being Interval
for y being real number st B is left_open_interval holds
y ++ B is left_open_interval

proof

let B be Interval; :: thesis: for y being real number st B is left_open_interval holds
y ++ B is left_open_interval
let y be real number ; :: thesis: ( B is left_open_interval implies y ++ B is left_open_interval )
reconsider y = y as Real by XREAL_0:def 1;
reconsider z = y as R_eal by XXREAL_0:def 1;
assume B is left_open_interval ; :: thesis: y ++ B is left_open_interval
then consider a being R_eal, b1 being real number such that
A2: ( a <= b1 & B = ].a,b1.] ) by MEASURE5:def 8;
reconsider t1 = y + b1 as Real ;
reconsider b = b1 as R_eal by XXREAL_0:def 1;
set s = z + a;
set t = z + b;
A3: z + a <= z + b by A2, XXREAL_3:38;
y ++ B = ].(z + a),(z + b).]

proof

thus y ++ B c= ].(z + a),(z + b).] :: according to XBOOLE_0:def 10 :: thesis: ].(z + a),(z + b).] c= y ++ B

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in y ++ B or c in ].(z + a),(z + b).] )
assume A4: c in y ++ B ; :: thesis: c in ].(z + a),(z + b).]
then reconsider c = c as Real ;
consider d being Real such that
A5: ( d in B & c = y + d ) by A4, Def6;
reconsider d1 = d as R_eal by XXREAL_0:def 1;
( a < d1 & d1 <= b & d1 in REAL ) by A2, A5, XXREAL_1:2;
then A6: ( z + a < z + d1 & z + d1 <= z + b ) by XXREAL_3:38, XXREAL_3:47;
z + d1 = c by A5, SUPINF_2:1;
hence c in ].(z + a),(z + b).] by A6, XXREAL_1:2; :: thesis: verum

end;

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in ].(z + a),(z + b).] or c in y ++ B )
assume A7: c in ].(z + a),(z + b).] ; :: thesis: c in y ++ B
then reconsider c = c as Real by XREAL_0:def 1;
reconsider c1 = c as R_eal by XXREAL_0:def 1;
( z + a < c1 & c1 <= z + b ) by A7, XXREAL_1:2;
then ( (a + z) - z < c1 - z & c1 - z <= (b + z) - z ) by XXREAL_3:38, XXREAL_3:47;
then A8: ( a < c1 - z & c1 - z <= b ) by XXREAL_3:22;
c1 - z = c - y by SUPINF_2:5;
then ( c - y in B & c = y + (c - y) ) by A2, A8, XXREAL_1:2;
hence c in y ++ B by Def6; :: thesis: verum

end;

hence y ++ B is left_open_interval by A3, MEASURE5:def 8; :: thesis: verum

end;

( x ++ A is left_open_interval implies A is left_open_interval )

proof

assume A9: x ++ A is left_open_interval ; :: thesis: A is left_open_interval
then reconsider B = x ++ A as Interval by MEASURE5:def 9;
reconsider y = - x as Real by XREAL_0:def 1;
y ++ B = A by Th59;
hence A is left_open_interval by A1, A9; :: thesis: verum

end;

hence ( A is left_open_interval iff x ++ A is left_open_interval ) by A1; :: thesis: verum