fof(t17_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( l1_metric_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k4_subset_1(u1_struct_0(B),k11_metric_1(B,C,A),k9_metric_1(B,C,A)) = k10_metric_1(B,C,A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_metric_1,t16_metric_1,t8_xboole_1,d10_xboole_0,d17_metric_1,t13_metric_1,t12_metric_1,t14_metric_1,d5_real_1,d2_xboole_0,t7_subset_1,d15_metric_1,d16_metric_1,d17_metric_1]),
    [file(metric_1,t17_metric_1),interesting(1.00)]).

fof(t15_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( l1_metric_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => r1_tarski(k9_metric_1(B,C,A),k10_metric_1(B,C,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_metric_1,t12_metric_1,l35_metric_1,t7_subset_1,d15_metric_1,d16_metric_1]),
    [file(metric_1,t15_metric_1),interesting(0.97)]).

fof(t16_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( l1_metric_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => r1_tarski(k11_metric_1(B,C,A),k10_metric_1(B,C,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_metric_1,t14_metric_1,l35_metric_1,t7_subset_1,d16_metric_1,d17_metric_1]),
    [file(metric_1,t16_metric_1),interesting(0.97)]).

fof(l4_metric_1,theorem,(
    k1_binop_1(k3_metric_1,k1_xboole_0,k1_xboole_0) = 0 ),
    inference(mizar_proof,[status(thm)],[l3_metric_1,t13_funcop_1]),
    [file(metric_1,l4_metric_1),interesting(0.92)]).

fof(l3_metric_1,theorem,(
    r2_hidden(k4_tarski(k1_xboole_0,k1_xboole_0),k2_zfmisc_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0))) ),
    inference(mizar_proof,[status(thm)],[t34_zfmisc_1]),
    [file(metric_1,l3_metric_1),interesting(0.84)]).

fof(l34_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_metric_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k9_metric_1(B,C,A) = a_3_0_metric_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_metric_1]),
    [file(metric_1,l34_metric_1),interesting(0.78)]).

fof(l35_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_metric_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k10_metric_1(B,C,A) = a_3_1_metric_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_metric_1]),
    [file(metric_1,l35_metric_1),interesting(0.78)]).

fof(l36_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_metric_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k11_metric_1(B,C,A) = a_3_2_metric_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_metric_1]),
    [file(metric_1,l36_metric_1),interesting(0.78)]).

fof(t1_metric_1,theorem,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => k2_metric_1(A,B,B) = 0 )
      <=> v6_metric_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_metric_1,d7_metric_1,d7_metric_1,d3_metric_1]),
    [file(metric_1,t1_metric_1),interesting(0.77)]).

fof(t10_metric_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => k1_metric_1(k1_numbers,k1_numbers,k7_metric_1,A,B) = k1_metric_1(k1_numbers,k1_numbers,k7_metric_1,B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_metric_1,t138_complex1,d13_metric_1]),
    [file(metric_1,t10_metric_1),interesting(0.70)]).

fof(t9_metric_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( k1_metric_1(k1_numbers,k1_numbers,k7_metric_1,A,B) = 0
          <=> A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_metric_1,t7_absvalue,t7_absvalue,d13_metric_1]),
    [file(metric_1,t9_metric_1),interesting(0.70)]).

fof(t14_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( l1_metric_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( r2_hidden(D,k11_metric_1(B,C,A))
                  <=> ( ~ v3_struct_0(B)
                      & k2_metric_1(B,C,D) = A ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_struct_0,l36_metric_1,l36_metric_1]),
    [file(metric_1,t14_metric_1),interesting(0.69)]).

fof(t3_metric_1,theorem,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k2_metric_1(A,B,C) = k2_metric_1(A,C,B) ) )
      <=> v8_metric_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_metric_1,d9_metric_1,d9_metric_1,d5_metric_1]),
    [file(metric_1,t3_metric_1),interesting(0.69)]).

fof(t4_metric_1,theorem,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => r1_xreal_0(k2_metric_1(A,B,D),k3_real_1(k2_metric_1(A,B,C),k2_metric_1(A,C,D))) ) ) )
      <=> v9_metric_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_metric_1,d10_metric_1,d10_metric_1,d6_metric_1]),
    [file(metric_1,t4_metric_1),interesting(0.69)]).

fof(t12_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( l1_metric_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( r2_hidden(D,k9_metric_1(B,C,A))
                  <=> ( ~ v3_struct_0(B)
                      & ~ r1_xreal_0(A,k2_metric_1(B,C,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_struct_0,l34_metric_1,l34_metric_1]),
    [file(metric_1,t12_metric_1),interesting(0.68)]).

fof(t13_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( l1_metric_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( r2_hidden(D,k10_metric_1(B,C,A))
                  <=> ( ~ v3_struct_0(B)
                      & r1_xreal_0(k2_metric_1(B,C,D),A) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_struct_0,l35_metric_1,l35_metric_1]),
    [file(metric_1,t13_metric_1),interesting(0.68)]).

fof(t18_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_metric_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k9_metric_1(B,C,A) = a_3_0_metric_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l34_metric_1]),
    [file(metric_1,t18_metric_1),interesting(0.68)]).

fof(t19_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_metric_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k10_metric_1(B,C,A) = a_3_1_metric_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l35_metric_1]),
    [file(metric_1,t19_metric_1),interesting(0.68)]).

fof(t20_metric_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_metric_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k11_metric_1(B,C,A) = a_3_2_metric_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l36_metric_1]),
    [file(metric_1,t20_metric_1),interesting(0.68)]).

fof(t2_metric_1,theorem,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( k2_metric_1(A,B,C) = 0
                 => B = C ) ) )
      <=> v7_metric_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_metric_1,d8_metric_1,d8_metric_1,d4_metric_1]),
    [file(metric_1,t2_metric_1),interesting(0.61)]).

fof(l5_metric_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_tarski(k1_xboole_0))
     => ! [B] : 
          ( m1_subset_1(B,k1_tarski(k1_xboole_0))
         => ( k1_metric_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0),k3_metric_1,A,B) = 0
          <=> A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,l4_metric_1]),
    [file(metric_1,l5_metric_1),interesting(0.58)]).

fof(l6_metric_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_tarski(k1_xboole_0))
     => ! [B] : 
          ( m1_subset_1(B,k1_tarski(k1_xboole_0))
         => k1_metric_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0),k3_metric_1,A,B) = k1_metric_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0),k3_metric_1,B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski]),
    [file(metric_1,l6_metric_1),interesting(0.53)]).

fof(t5_metric_1,theorem,(
    ! [A] : 
      ( ( v6_metric_1(A)
        & v8_metric_1(A)
        & v9_metric_1(A)
        & l1_metric_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => r1_xreal_0(0,k4_metric_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_metric_1,t1_metric_1,t66_xreal_1]),
    [file(metric_1,t5_metric_1),interesting(0.53)]).

fof(l7_metric_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_tarski(k1_xboole_0))
     => ! [B] : 
          ( m1_subset_1(B,k1_tarski(k1_xboole_0))
         => ! [C] : 
              ( m1_subset_1(C,k1_tarski(k1_xboole_0))
             => r1_xreal_0(k1_metric_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0),k3_metric_1,A,C),k3_real_1(k1_metric_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0),k3_metric_1,A,B),k1_metric_1(k1_tarski(k1_xboole_0),k1_tarski(k1_xboole_0),k3_metric_1,B,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,l4_metric_1]),
    [file(metric_1,l7_metric_1),interesting(0.39)]).

fof(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [interesting(0.00)]).

fof(t34_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(k1_tarski(C),k1_tarski(D)))
    <=> ( A = C
        & B = D ) ) ),
    file(zfmisc_1,t34_zfmisc_1),
    [interesting(0.00)]).

fof(t13_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(B,A)
     => k1_funct_1(k2_funcop_1(A,C),B) = C ) ),
    file(funcop_1,t13_funcop_1),
    [interesting(0.00)]).

fof(d13_metric_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers)
        & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) )
     => ( A = k7_metric_1
      <=> ! [B] : 
            ( m1_subset_1(B,k1_numbers)
           => ! [C] : 
                ( m1_subset_1(C,k1_numbers)
               => k1_metric_1(k1_numbers,k1_numbers,A,B,C) = k18_complex1(k5_real_1(B,C)) ) ) ) ) ),
    file(metric_1,d13_metric_1),
    [interesting(0.00)]).

fof(t138_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ),
    file(complex1,t138_complex1),
    [interesting(0.00)]).

fof(t142_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => r1_xreal_0(k17_complex1(k2_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ),
    file(complex1,t142_complex1),
    [interesting(0.00)]).

fof(t11_metric_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => r1_xreal_0(k1_metric_1(k1_numbers,k1_numbers,k7_metric_1,A,B),k3_real_1(k1_metric_1(k1_numbers,k1_numbers,k7_metric_1,A,C),k1_metric_1(k1_numbers,k1_numbers,k7_metric_1,C,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t142_complex1,d13_metric_1]),
    [file(metric_1,t11_metric_1),interesting(0.00)]).

fof(d15_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                 => ( ( ~ v3_struct_0(A)
                     => ( D = k9_metric_1(A,B,C)
                      <=> ? [E] : 
                            ( ~ v3_struct_0(E)
                            & l1_metric_1(E)
                            & ? [F] : 
                                ( m1_subset_1(F,u1_struct_0(E))
                                & E = A
                                & F = B
                                & D = a_3_0_metric_1(C,E,F) ) ) ) )
                    & ( v3_struct_0(A)
                     => ( D = k9_metric_1(A,B,C)
                      <=> v1_xboole_0(D) ) ) ) ) ) ) ) ),
    file(metric_1,d15_metric_1),
    [interesting(0.00)]).

fof(d1_struct_0,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => ( v3_struct_0(A)
      <=> v1_xboole_0(u1_struct_0(A)) ) ) ),
    file(struct_0,d1_struct_0),
    [interesting(0.00)]).

fof(d16_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                 => ( ( ~ v3_struct_0(A)
                     => ( D = k10_metric_1(A,B,C)
                      <=> ? [E] : 
                            ( ~ v3_struct_0(E)
                            & l1_metric_1(E)
                            & ? [F] : 
                                ( m1_subset_1(F,u1_struct_0(E))
                                & E = A
                                & F = B
                                & D = a_3_1_metric_1(C,E,F) ) ) ) )
                    & ( v3_struct_0(A)
                     => ( D = k10_metric_1(A,B,C)
                      <=> v1_xboole_0(D) ) ) ) ) ) ) ) ),
    file(metric_1,d16_metric_1),
    [interesting(0.00)]).

fof(t7_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( ! [D] : 
                ( m1_subset_1(D,A)
               => ( r2_hidden(D,B)
                 => r2_hidden(D,C) ) )
           => r1_tarski(B,C) ) ) ) ),
    file(subset_1,t7_subset_1),
    [interesting(0.00)]).

fof(d17_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                 => ( ( ~ v3_struct_0(A)
                     => ( D = k11_metric_1(A,B,C)
                      <=> ? [E] : 
                            ( ~ v3_struct_0(E)
                            & l1_metric_1(E)
                            & ? [F] : 
                                ( m1_subset_1(F,u1_struct_0(E))
                                & E = A
                                & F = B
                                & D = a_3_2_metric_1(C,E,F) ) ) ) )
                    & ( v3_struct_0(A)
                     => ( D = k11_metric_1(A,B,C)
                      <=> v1_xboole_0(D) ) ) ) ) ) ) ) ),
    file(metric_1,d17_metric_1),
    [interesting(0.00)]).

fof(t8_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,B) )
     => r1_tarski(k2_xboole_0(A,C),B) ) ),
    file(xboole_1,t8_xboole_1),
    [interesting(0.00)]).

fof(d10_xboole_0,definition,(
    ! [A,B] : 
      ( A = B
    <=> ( r1_tarski(A,B)
        & r1_tarski(B,A) ) ) ),
    file(xboole_0,d10_xboole_0),
    [interesting(0.00)]).

fof(d5_real_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
          <=> ~ ( r1_xreal_0(B,A)
                & B != A ) ) ) ) ),
    file(real_1,d5_real_1),
    [interesting(0.00)]).

fof(d2_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k2_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            | r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d2_xboole_0),
    [interesting(0.00)]).

fof(d4_metric_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k2_zfmisc_1(A,A),k1_numbers) )
     => ( v3_metric_1(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,A)
           => ! [D] : 
                ( m1_subset_1(D,A)
               => ( k1_metric_1(A,A,B,C,D) = 0
                 => C = D ) ) ) ) ) ),
    file(metric_1,d4_metric_1),
    [interesting(0.00)]).

fof(d8_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( v7_metric_1(A)
      <=> v3_metric_1(u1_metric_1(A),u1_struct_0(A)) ) ) ),
    file(metric_1,d8_metric_1),
    [interesting(0.00)]).

fof(d5_metric_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k2_zfmisc_1(A,A),k1_numbers) )
     => ( v4_metric_1(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,A)
           => ! [D] : 
                ( m1_subset_1(D,A)
               => k1_metric_1(A,A,B,C,D) = k1_metric_1(A,A,B,D,C) ) ) ) ) ),
    file(metric_1,d5_metric_1),
    [interesting(0.00)]).

fof(d9_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( v8_metric_1(A)
      <=> v4_metric_1(u1_metric_1(A),u1_struct_0(A)) ) ) ),
    file(metric_1,d9_metric_1),
    [interesting(0.00)]).

fof(d6_metric_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k2_zfmisc_1(A,A),k1_numbers) )
     => ( v5_metric_1(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,A)
           => ! [D] : 
                ( m1_subset_1(D,A)
               => ! [E] : 
                    ( m1_subset_1(E,A)
                   => r1_xreal_0(k1_metric_1(A,A,B,C,E),k3_real_1(k1_metric_1(A,A,B,C,D),k1_metric_1(A,A,B,D,E))) ) ) ) ) ) ),
    file(metric_1,d6_metric_1),
    [interesting(0.00)]).

fof(d10_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( v9_metric_1(A)
      <=> v5_metric_1(u1_metric_1(A),u1_struct_0(A)) ) ) ),
    file(metric_1,d10_metric_1),
    [interesting(0.00)]).

fof(d3_metric_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k2_zfmisc_1(A,A),k1_numbers) )
     => ( v2_metric_1(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,A)
           => k1_metric_1(A,A,B,C,C) = 0 ) ) ) ),
    file(metric_1,d3_metric_1),
    [interesting(0.00)]).

fof(d7_metric_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( v6_metric_1(A)
      <=> v2_metric_1(u1_metric_1(A),u1_struct_0(A)) ) ) ),
    file(metric_1,d7_metric_1),
    [interesting(0.00)]).

fof(t66_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ( r1_xreal_0(A,B)
                  & r1_xreal_0(0,C) )
               => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t66_xreal_1),
    [interesting(0.00)]).

fof(t6_metric_1,theorem,(
    ! [A] : 
      ( l1_metric_1(A)
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( ( k2_metric_1(A,B,C) = 0
                       => B = C )
                      & ( B = C
                       => k2_metric_1(A,B,C) = 0 )
                      & k2_metric_1(A,B,C) = k2_metric_1(A,C,B)
                      & r1_xreal_0(k2_metric_1(A,B,D),k3_real_1(k2_metric_1(A,B,C),k2_metric_1(A,C,D))) ) ) ) )
       => ( v6_metric_1(A)
          & v7_metric_1(A)
          & v8_metric_1(A)
          & v9_metric_1(A)
          & l1_metric_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_metric_1,d7_metric_1,d4_metric_1,d8_metric_1,d5_metric_1,d9_metric_1,d6_metric_1,d10_metric_1]),
    [file(metric_1,t6_metric_1),interesting(0.00)]).

fof(t7_metric_1,theorem,(
    $true ),
    file(metric_1,t7_metric_1),
    [interesting(0.00)]).

fof(t8_metric_1,theorem,(
    $true ),
    file(metric_1,t8_metric_1),
    [interesting(0.00)]).

fof(t7_absvalue,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( A = 0
      <=> k18_complex1(A) = 0 ) ) ),
    file(absvalue,t7_absvalue),
    [interesting(0.00)]).