let n be Element of NAT ; :: thesis: for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x + z),A <= (dist x,A) + |.z.|
let x, z be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) st A <> {} holds
dist (x + z),A <= (dist x,A) + |.z.|
let A be Subset of (COMPLEX n); :: thesis: ( A <> {} implies dist (x + z),A <= (dist x,A) + |.z.| )
assume A <> {} ; :: thesis: dist (x + z),A <= (dist x,A) + |.z.|
then consider z2 being Element of COMPLEX n such that
A1: z2 in A by SUBSET_1:10;
defpred S₁[ set ] means $1 in A;
deffunc H₁( Element of COMPLEX n) -> Real = |.(x - $1).|;
deffunc H₂( Element of COMPLEX n) -> Real = |.((x + z) - $1).|;
reconsider X = { H₁(z1) where z1 is Element of COMPLEX n : S₁[z1] } as Subset of REAL from COMPLSP1:sch 1();
reconsider Y = { H₂(z1) where z1 is Element of COMPLEX n : S₁[z1] } as Subset of REAL from COMPLSP1:sch 1();
A2: dist x,A = lower_bound X by Def18;
A3: dist (x + z),A = lower_bound Y by Def18;
A4: |.(x - z2).| in X by A1;
A5: Y is bounded_below

proof

take 0 ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in Y or 0 <= b₁ )
let r be real number ; :: thesis: ( not r in Y or 0 <= r )
assume r in Y ; :: thesis: 0 <= r
then ex z1 being Element of COMPLEX n st
( r = |.((x + z) - z1).| & z1 in A ) ;
hence 0 <= r by Th65; :: thesis: verum

end;

now

let r' be Real; :: thesis: ( r' in X implies r' >= (dist (x + z),A) - |.z.| )
assume r' in X ; :: thesis: r' >= (dist (x + z),A) - |.z.|
then consider z3 being Element of COMPLEX n such that
A6: ( r' = |.(x - z3).| & z3 in A ) ;
|.((x + z) - z3).| in Y by A6;
then A7: |.((x + z) - z3).| >= dist (x + z),A by A3, A5, SEQ_4:def 5;
|.((x + z) - z3).| = |.((x - z3) + z).| by Th46;
then |.((x + z) - z3).| <= r' + |.z.| by A6, Th68;
then r' + |.z.| >= dist (x + z),A by A7, XXREAL_0:2;
hence r' >= (dist (x + z),A) - |.z.| by XREAL_1:22; :: thesis: verum

end;

then (dist (x + z),A) - |.z.| <= dist x,A by A2, A4, Th84;
hence dist (x + z),A <= (dist x,A) + |.z.| by XREAL_1:22; :: thesis: verum