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

proof

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

end;

A6: ( X <> {} & X is bounded_below )

proof

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

end;

A7: ( Y <> {} & Y is bounded_below )

proof

|.(x - z2).| in Y by A3;
hence Y <> {} ; :: thesis: Y is bounded_below
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 - z1).| & z1 in B ) ;
hence 0 <= r by Th65; :: thesis: verum

end;

now

let r be Real; :: thesis: ( r in X + Y implies ex r3 being Real st
( r3 in Z & r3 <= r ) )
assume r in X + Y ; :: thesis: ex r3 being Real st
( r3 in Z & r3 <= r )
then consider r2, r1 being Real such that
A8: r = r2 + r1 and
A9: ( r2 in X & r1 in Y ) ;
consider z1 being Element of COMPLEX n such that
A10: r2 = |.(x - z1).| and
A11: z1 in A by A9;
consider z2 being Element of COMPLEX n such that
A12: ( r1 = |.(x - z2).| & z2 in B ) by A9;
take r3 = |.(z1 - z2).|; :: thesis: ( r3 in Z & r3 <= r )
r2 = |.(z1 - x).| by A10, Th74;
hence ( r3 in Z & r3 <= r ) by A8, A11, A12, Th75; :: thesis: verum

end;

then A13: lower_bound (X + Y) >= lower_bound Z by A4, A5, Th97;
( lower_bound X = dist x,A & lower_bound Y = dist x,B & lower_bound Z = dist A,B ) by Def18, Def20;
hence (dist x,A) + (dist x,B) >= dist A,B by A6, A7, A13, Th96; :: thesis: verum