let A be real-membered set ; :: thesis: for x being Real
for y being R_eal st x = y holds
inf (x ++ A) = y + (inf A)
let x be Real; :: thesis: for y being R_eal st x = y holds
inf (x ++ A) = y + (inf A)
let y be R_eal; :: thesis: ( x = y implies inf (x ++ A) = y + (inf A) )
assume A1: x = y ; :: thesis: inf (x ++ A) = y + (inf A)
A2: for z being LowerBound of x ++ A holds z <= y + (inf A)

proof

let z be LowerBound of x ++ A; :: thesis: z <= y + (inf A)
reconsider zz = z as R_eal by XXREAL_0:def 1;
zz - y is LowerBound of A

proof

let u be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not u in A or zz - y <= u )
reconsider uu = u as R_eal by XXREAL_0:def 1;
assume A3: u in A ; :: thesis: zz - y <= u
then reconsider u1 = u as Real ;
y + uu = x + u1 by A1, XXREAL_3:def 2;
then y + uu in x ++ A by A3, Lm1;
then z <= y + uu by XXREAL_2:def 2;
hence zz - y <= u by A1, XXREAL_3:42; :: thesis: verum

end;

then zz - y <= inf A by XXREAL_2:def 4;
hence z <= y + (inf A) by A1, XXREAL_3:41; :: thesis: verum

end;

y + (inf A) is LowerBound of x ++ A

proof

let z be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not z in x ++ A or y + (inf A) <= z )
assume z in x ++ A ; :: thesis: y + (inf A) <= z
then consider a being Real such that
A4: a in A and
A5: z = x + a by Lm1;
reconsider b = a as R_eal by XXREAL_0:def 1;
A6: inf A <= a by A4, XXREAL_2:3;
ex a, c being Complex st
( y = a & b = c & y + b = a + c ) by A1, XXREAL_3:def 2;
hence y + (inf A) <= z by A1, A5, A6, XXREAL_3:36; :: thesis: verum

end;

hence inf (x ++ A) = y + (inf A) by A2, XXREAL_2:def 4; :: thesis: verum