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

proof

let B be Interval; :: thesis: for y being Real st B is closed_interval holds
y ++ B is closed_interval
let y be Real; :: thesis: ( B is closed_interval implies y ++ B is closed_interval )
reconsider y = y as Real ;
reconsider z = y as R_eal by XXREAL_0:def 1;
assume B is closed_interval ; :: thesis: y ++ B is closed_interval
then consider a1, b1 being Real such that
A2: B = [.a1,b1.] by MEASURE5:def 3;
reconsider a = a1, b = b1 as R_eal by XXREAL_0:def 1;
reconsider s = z + a, t = z + b as R_eal ;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not c in y ++ B or c in [.s,t.] )
assume A3: c in y ++ B ; :: thesis: c in [.s,t.]
then reconsider c = c as Real ;
consider d being Real such that
A4: d in B and
A5: c = y + d by A3, Lm1;
reconsider d1 = d as R_eal by XXREAL_0:def 1;
a <= d1 by A2, A4, XXREAL_1:1;
then A6: s <= z + d1 by XXREAL_3:36;
d1 <= b by A2, A4, XXREAL_1:1;
then A7: z + d1 <= t by XXREAL_3:36;
z + d1 = c by A5, SUPINF_2:1;
hence c in [.s,t.] by A6, A7, XXREAL_1:1; :: thesis: verum

end;

reconsider a = a, b = b as R_eal ;
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in [.s,t.] or c in y ++ B )
assume A8: c in [.s,t.] ; :: thesis: c in y ++ B
then reconsider c = c as Real ;
reconsider c1 = c as R_eal by XXREAL_0:def 1;
A9: c = y + (c - y) ;
c1 <= z + b by A8, XXREAL_1:1;
then c1 - z <= (b + z) - z by XXREAL_3:36;
then A10: c1 - z <= b by XXREAL_3:22;
z + a <= c1 by A8, XXREAL_1:1;
then (a + z) - z <= c1 - z by XXREAL_3:36;
then A11: a <= c1 - z by XXREAL_3:22;
c1 - z = c - y by SUPINF_2:3;
then c - y in B by A2, A11, A10;
hence c in y ++ B by A9, Lm1; :: thesis: verum

end;

hence y ++ B is closed_interval by MEASURE5:def 3; :: thesis: verum

end;

( x ++ A is closed_interval implies A is closed_interval )

proof

reconsider y = - x as Real ;
assume A12: x ++ A is closed_interval ; :: thesis: A is closed_interval
then reconsider B = x ++ A as Interval ;
y ++ B = A by Th23;
hence A is closed_interval by A1, A12; :: thesis: verum

end;

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