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

proof

let B be Interval; :: thesis: for y being real number st B is right_open_interval holds
y ++ B is right_open_interval
let y be real number ; :: thesis: ( B is right_open_interval implies y ++ B is right_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 right_open_interval ; :: thesis: y ++ B is right_open_interval
then consider a1 being real number , b being R_eal such that
A2: a1 <= b and
A3: B = [.a1,b.[ by MEASURE5:def 7;
reconsider a = a1 as R_eal by XXREAL_0:def 1;
reconsider s = z + a, t = z + b as R_eal ;
A4: y ++ B = [.s,t.[

proof

thus y ++ B c= [.s,t.[ :: according to XBOOLE_0:def 10 :: thesis: [.s,t.[ c= y ++ B

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in y ++ B or c in [.s,t.[ )
assume A5: c in y ++ B ; :: thesis: c in [.s,t.[
then reconsider c = c as Real ;
consider d being Real such that
A6: d in B and
A7: c = y + d by A5, Def6;
reconsider d1 = d as R_eal by XXREAL_0:def 1;
a <= d1 by A3, A6, XXREAL_1:3;
then A8: s <= z + d1 by XXREAL_3:38;
d1 < b by A3, A6, XXREAL_1:3;
then A9: z + d1 < t by XXREAL_3:47;
z + d1 = c by A7, SUPINF_2:1;
hence c in [.s,t.[ by A8, A9, XXREAL_1:3; :: thesis: verum

end;

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in [.s,t.[ or c in y ++ B )
assume A10: c in [.s,t.[ ; :: 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;
A11: c = y + (c - y) ;
c1 < z + b by A10, XXREAL_1:3;
then c1 - z < (b + z) - z by XXREAL_3:47;
then A12: c1 - z < b by XXREAL_3:22;
z + a <= c1 by A10, XXREAL_1:3;
then (a + z) - z <= c1 - z by XXREAL_3:38;
then A13: a <= c1 - z by XXREAL_3:22;
c1 - z = c - y by SUPINF_2:5;
then c - y in B by A3, A13, A12, XXREAL_1:3;
hence c in y ++ B by A11, Def6; :: thesis: verum

end;

s <= t by A2, XXREAL_3:38;
hence y ++ B is right_open_interval by A4, MEASURE5:def 7; :: thesis: verum
reconsider s1 = y + a1 as Real ;

end;

( x ++ A is right_open_interval implies A is right_open_interval )

proof

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

end;

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