fof(t1_ali2,theorem,(
    $true ),
    file(ali2,t1_ali2),
    [interesting(0.00)]).

fof(d1_ali2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_metric_1(A)
        & v7_metric_1(A)
        & v8_metric_1(A)
        & v9_metric_1(A)
        & l1_metric_1(A) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
            & m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
         => ( m1_ali2(B,A)
          <=> ? [C] : 
                ( m1_subset_1(C,k1_numbers)
                & ~ r1_xreal_0(C,0)
                & ~ r1_xreal_0(1,C)
                & ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(A))
                       => r1_xreal_0(k4_metric_1(A,k8_funct_2(u1_struct_0(A),u1_struct_0(A),B,D),k8_funct_2(u1_struct_0(A),u1_struct_0(A),B,E)),k4_real_1(C,k4_metric_1(A,D,E))) ) ) ) ) ) ) ),
    file(ali2,d1_ali2),
    [interesting(0.00)]).

fof(s3_subset_1,theorem,(
    ? [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(f1_s3_subset_1))
      & ! [B] : 
          ( m1_subset_1(B,f1_s3_subset_1)
         => ( r2_hidden(B,A)
          <=> p1_s3_subset_1(B) ) ) ) ),
    file(subset_1,s3_subset_1),
    [interesting(0.00)]).

fof(d6_pcomps_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => k5_pcomps_1(A) = g1_pre_topc(u1_struct_0(A),k4_pcomps_1(A)) ) ),
    file(pcomps_1,d6_pcomps_1),
    [interesting(0.00)]).

fof(s7_domain_1,theorem,(
    m1_subset_1(a_0_0_domain_1,k1_zfmisc_1(f1_s7_domain_1)) ),
    file(domain_1,s7_domain_1),
    [interesting(0.00)]).

fof(d2_compts_1,definition,(
    ! [A] : 
      ( v1_compts_1(A)
    <=> ( A != k1_xboole_0
        & ! [B] : ~ ( B != k1_xboole_0
            & r1_tarski(B,A)
            & v1_finset_1(B)
            & k1_setfam_1(B) = k1_xboole_0 ) ) ) ),
    file(compts_1,d2_compts_1),
    [interesting(0.00)]).

fof(d9_ordinal1,definition,(
    ! [A] : 
      ( v6_ordinal1(A)
    <=> ! [B,C] : 
          ( ( r2_hidden(B,A)
            & r2_hidden(C,A) )
         => r3_xboole_0(B,C) ) ) ),
    file(ordinal1,d9_ordinal1),
    [interesting(0.00)]).

fof(t45_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(B,A)
                  & ~ r1_xreal_0(C,0)
                  & ~ r1_xreal_0(1,C)
                  & r1_xreal_0(k3_power(C,A),k3_power(C,B)) ) ) ) ) ),
    file(power,t45_power),
    [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(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)) ) ) ) ),
    file(metric_1,t5_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(d3_tarski,definition,(
    ! [A,B] : 
      ( r1_tarski(A,B)
    <=> ! [C] : 
          ( r2_hidden(C,A)
         => r2_hidden(C,B) ) ) ),
    file(tarski,d3_tarski),
    [interesting(0.00)]).

fof(t2_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(B,C) )
               => r1_xreal_0(A,C) ) ) ) ) ),
    file(xreal_1,t2_xreal_1),
    [interesting(0.00)]).

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

fof(t30_finset_1,theorem,(
    ! [A] : ~ ( v1_finset_1(A)
      & A != k1_xboole_0
      & v6_ordinal1(A)
      & ! [B] : ~ ( r2_hidden(B,A)
          & ! [C] : 
              ( r2_hidden(C,A)
             => r1_tarski(B,C) ) ) ) ),
    file(finset_1,t30_finset_1),
    [interesting(0.00)]).

fof(t6_setfam_1,theorem,(
    ! [A,B] : 
      ( ! [C] : 
          ( r2_hidden(C,A)
         => r1_tarski(B,C) )
     => ( A = k1_xboole_0
        | r1_tarski(B,k1_setfam_1(A)) ) ) ),
    file(setfam_1,t6_setfam_1),
    [interesting(0.00)]).

fof(t29_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,0) = 1 ) ),
    file(power,t29_power),
    [interesting(0.00)]).

fof(t30_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,1) = A ) ),
    file(power,t30_power),
    [interesting(0.00)]).

fof(t32_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => k3_power(A,k2_xcmplx_0(B,C)) = k3_xcmplx_0(k3_power(A,B),k3_power(A,C)) ) ) ) ) ),
    file(power,t32_power),
    [interesting(0.00)]).

fof(s1_nat_1,theorem,
    ( ( p1_s1_nat_1(0)
      & ! [A] : 
          ( m2_subset_1(A,k1_numbers,k5_numbers)
         => ( p1_s1_nat_1(A)
           => p1_s1_nat_1(k1_nat_1(A,1)) ) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => p1_s1_nat_1(A) ) ),
    file(nat_1,s1_nat_1),
    [interesting(0.00)]).

fof(t3_xboole_1,theorem,(
    ! [A] : 
      ( r1_tarski(A,k1_xboole_0)
     => A = k1_xboole_0 ) ),
    file(xboole_1,t3_xboole_1),
    [interesting(0.00)]).

fof(d2_tops_2,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
         => ( v2_tops_2(B,A)
          <=> ! [C] : 
                ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
               => ( r2_hidden(C,B)
                 => v4_pre_topc(C,A) ) ) ) ) ) ),
    file(tops_2,d2_tops_2),
    [interesting(0.00)]).

fof(t54_subset_1,theorem,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k1_zfmisc_1(A))
     => ~ ( r2_hidden(B,k3_subset_1(A,C))
          & r2_hidden(B,C) ) ) ),
    file(subset_1,t54_subset_1),
    [interesting(0.00)]).

fof(t52_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(B,A)
              & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ),
    file(xreal_1,t52_xreal_1),
    [interesting(0.00)]).

fof(t3_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ~ r1_xreal_0(A,0)
       => ( ~ r1_xreal_0(k7_xcmplx_0(A,2),0)
          & ~ r1_xreal_0(k7_xcmplx_0(A,4),0) ) ) ) ),
    file(seq_2,t3_seq_2),
    [interesting(0.00)]).

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)) ) ) ) ) ) ) ),
    file(metric_1,t12_metric_1),
    [interesting(0.00)]).

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) ) ) ),
    file(metric_1,t4_metric_1),
    [interesting(0.00)]).

fof(t8_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(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t8_xreal_1),
    [interesting(0.00)]).

fof(t147_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( ( r1_xreal_0(0,A)
                & r1_xreal_0(B,1) )
              | ( r1_xreal_0(A,0)
                & r1_xreal_0(1,B) ) )
           => r1_xreal_0(k3_xcmplx_0(A,B),A) ) ) ) ),
    file(real_2,t147_real_2),
    [interesting(0.00)]).

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

fof(t9_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ( ( r1_xreal_0(A,B)
                      & r1_xreal_0(C,D) )
                   => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ),
    file(xreal_1,t9_xreal_1),
    [interesting(0.00)]).

fof(t21_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(k2_xcmplx_0(A,B),C)
              <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ),
    file(xreal_1,t21_xreal_1),
    [interesting(0.00)]).

fof(t50_subset_1,theorem,(
    ! [A] : 
      ( A != k1_xboole_0
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ( ~ r2_hidden(C,B)
               => r2_hidden(C,k3_subset_1(A,B)) ) ) ) ) ),
    file(subset_1,t50_subset_1),
    [interesting(0.00)]).

fof(d5_pcomps_1,definition,(
    ! [A] : 
      ( l1_metric_1(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
         => ( B = k4_pcomps_1(A)
          <=> ! [C] : 
                ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
               => ( r2_hidden(C,B)
                <=> ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => ~ ( r2_hidden(D,C)
                          & ! [E] : 
                              ( m1_subset_1(E,k1_numbers)
                             => ~ ( ~ r1_xreal_0(E,0)
                                  & r1_tarski(k9_metric_1(A,D,E),C) ) ) ) ) ) ) ) ) ) ),
    file(pcomps_1,d5_pcomps_1),
    [interesting(0.00)]).

fof(d5_pre_topc,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ( v3_pre_topc(B,A)
          <=> r2_hidden(B,u1_pre_topc(A)) ) ) ) ),
    file(pre_topc,d5_pre_topc),
    [interesting(0.00)]).

fof(t29_tops_1,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ( v4_pre_topc(B,A)
          <=> v3_pre_topc(k3_subset_1(u1_struct_0(A),B),A) ) ) ) ),
    file(tops_1,t29_tops_1),
    [interesting(0.00)]).

fof(t13_compts_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ( v2_compts_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
           => ~ ( v1_compts_1(B)
                & v2_tops_2(B,A)
                & k6_setfam_1(u1_struct_0(A),B) = k1_xboole_0 ) ) ) ) ),
    file(compts_1,t13_compts_1),
    [interesting(0.00)]).

fof(t10_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ~ ( B != k1_xboole_0
          & ! [C] : 
              ( m1_subset_1(C,A)
             => ~ r2_hidden(C,B) ) ) ) ),
    file(subset_1,t10_subset_1),
    [interesting(0.00)]).

fof(s1_seq_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => k2_seq_1(k5_numbers,k1_numbers,A,B) = f1_s1_seq_1(B) ) ) ),
    file(seq_1,s1_seq_1),
    [interesting(0.00)]).

fof(t1_series_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k8_funct_2(k5_numbers,k1_numbers,B,C) = k3_power(A,k1_nat_1(C,1)) )
           => ( r1_xreal_0(A,0)
              | r1_xreal_0(1,A)
              | ( v4_seq_2(B)
                & k2_seq_2(B) = 0 ) ) ) ) ) ),
    file(series_1,t1_series_1),
    [interesting(0.00)]).

fof(t21_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(B)
           => v4_seq_2(k14_seq_1(B,A)) ) ) ) ),
    file(seq_2,t21_seq_2),
    [interesting(0.00)]).

fof(t22_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(B)
           => k2_seq_2(k14_seq_1(B,A)) = k3_xcmplx_0(A,k2_seq_2(B)) ) ) ) ),
    file(seq_2,t22_seq_2),
    [interesting(0.00)]).

fof(t57_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(C,B)
     => ( v1_funct_1(k2_funcop_1(A,C))
        & v1_funct_2(k2_funcop_1(A,C),A,B)
        & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ),
    file(funcop_1,t57_funcop_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(t39_seq_4,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v5_seqm_3(A)
       => v4_seq_2(A) ) ) ),
    file(seq_4,t39_seq_4),
    [interesting(0.00)]).

fof(d1_setfam_1,definition,(
    ! [A,B] : 
      ( ( A != k1_xboole_0
       => ( B = k1_setfam_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ! [D] : 
                  ( r2_hidden(D,A)
                 => r2_hidden(C,D) ) ) ) )
      & ( A = k1_xboole_0
       => ( B = k1_setfam_1(A)
        <=> B = k1_xboole_0 ) ) ) ),
    file(setfam_1,d1_setfam_1),
    [interesting(0.00)]).

fof(t13_seq_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( B = k14_seq_1(C,A)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,B,D) = k3_xcmplx_0(A,k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t13_seq_1),
    [interesting(0.00)]).

fof(t32_seq_2,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(A)
              & v4_seq_2(B)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,B,C)) ) )
           => r1_xreal_0(k2_seq_2(A),k2_seq_2(B)) ) ) ) ),
    file(seq_2,t32_seq_2),
    [interesting(0.00)]).

fof(t40_seq_4,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( ( v5_seqm_3(B)
                & r2_hidden(A,k2_relat_1(B)) )
              | ( v5_seqm_3(B)
                & ? [C] : 
                    ( m2_subset_1(C,k1_numbers,k5_numbers)
                    & k8_funct_2(k5_numbers,k1_numbers,B,C) = A ) ) )
           => k2_seq_2(B) = A ) ) ) ),
    file(seq_4,t40_seq_4),
    [interesting(0.00)]).

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) ) ) ),
    file(metric_1,t2_metric_1),
    [interesting(0.00)]).

fof(t145_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ( ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(1,B) )
                | ( ~ r1_xreal_0(0,A)
                  & ~ r1_xreal_0(B,1) ) )
              & r1_xreal_0(A,k3_xcmplx_0(A,B)) ) ) ) ),
    file(real_2,t145_real_2),
    [interesting(0.00)]).

fof(t2_ali2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_metric_1(A)
        & v7_metric_1(A)
        & v8_metric_1(A)
        & v9_metric_1(A)
        & l1_metric_1(A) )
     => ! [B] : 
          ( m1_ali2(B,A)
         => ~ ( v2_compts_1(k5_pcomps_1(A))
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( k8_funct_2(u1_struct_0(A),u1_struct_0(A),B,C) = C
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => ( k8_funct_2(u1_struct_0(A),u1_struct_0(A),B,D) = D
                           => D = C ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_ali2,s3_subset_1,d6_pcomps_1,s7_domain_1,d2_compts_1,d9_ordinal1,t45_power,d5_real_1,t5_metric_1,t66_xreal_1,d3_tarski,t2_xreal_1,d3_tarski,t2_xreal_1,d9_xboole_0,t30_finset_1,t6_setfam_1,t29_power,t66_xreal_1,t30_power,t32_power,t2_xreal_1,s1_nat_1,t3_xboole_1,d2_tops_2,d6_pcomps_1,t54_subset_1,t52_xreal_1,t3_seq_2,d3_tarski,t12_metric_1,t4_metric_1,t8_xreal_1,t4_metric_1,t2_xreal_1,t5_metric_1,t147_real_2,t2_xreal_1,t8_xreal_1,t70_xreal_1,t8_xreal_1,t9_xreal_1,t2_xreal_1,t2_xreal_1,t21_xreal_1,t50_subset_1,d5_pcomps_1,d5_pre_topc,t29_tops_1,t13_compts_1,t10_subset_1,s1_seq_1,t1_series_1,t21_seq_2,t22_seq_2,t57_funcop_1,t13_funcop_1,t39_seq_4,s7_domain_1,d1_setfam_1,t13_seq_1,t32_seq_2,t5_metric_1,t40_seq_4,t2_metric_1,t2_metric_1,t5_metric_1,t145_real_2]),
    [file(ali2,t2_ali2),interesting(0.00)]).