fof(t34_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => r1_xreal_0(1,k3_finseq_1(k10_qc_lang1(A))) ) ),
    inference(mizar_proof,[status(thm)],[t56_finseq_1,d17_qc_lang1,t23_qc_lang1,t35_finseq_1,t56_finseq_1,t29_nat_1,d18_qc_lang1,t35_finseq_1,t56_finseq_1,t29_nat_1,d19_qc_lang1,t45_finseq_1,t35_finseq_1,t56_finseq_1,t29_nat_1,d20_qc_lang1,t45_finseq_1,t35_finseq_1,t56_finseq_1,t29_nat_1,t33_qc_lang1]),
    [file(qc_lang1,t34_qc_lang1),interesting(1.00)]).

fof(t33_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ~ ( A != k11_qc_lang1
          & ~ v2_qc_lang1(A)
          & ~ v3_qc_lang1(A)
          & ~ v4_qc_lang1(A)
          & ~ v5_qc_lang1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_qc_lang1,d18_qc_lang1,d19_qc_lang1,d20_qc_lang1,s1_qc_lang1]),
    [file(qc_lang1,t33_qc_lang1),interesting(0.91)]).

fof(t37_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ! [B] : 
          ( m1_subset_1(B,k8_qc_lang1)
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( k10_qc_lang1(A) = k7_finseq_1(k10_qc_lang1(B),C)
               => k10_qc_lang1(A) = k10_qc_lang1(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_finseq_1,d3_finseq_1,t34_qc_lang1,t3_finseq_1,d7_finseq_1,t56_finseq_1,t34_qc_lang1,t29_nat_1,t1_xreal_1,t25_finseq_1,t47_finseq_1,d17_qc_lang1,t23_qc_lang1,t58_finseq_1,t36_qc_lang1,d17_qc_lang1,t23_qc_lang1,t58_finseq_1,d8_qc_lang1,t35_qc_lang1,t35_qc_lang1,d8_qc_lang1,t45_finseq_1,t46_finseq_1,t35_finseq_1,t25_finseq_1,t47_finseq_1,d18_qc_lang1,t58_finseq_1,t7_mcart_1,t36_qc_lang1,d18_qc_lang1,t45_finseq_1,t46_finseq_1,t35_finseq_1,t57_finseq_1,t38_nat_1,t47_finseq_1,t46_finseq_1,t47_finseq_1,d19_qc_lang1,t45_finseq_1,t58_finseq_1,t7_mcart_1,t36_qc_lang1,d19_qc_lang1,t45_finseq_1,t45_finseq_1,t46_finseq_1,t45_finseq_1,t64_finseq_1,t35_finseq_1,t57_finseq_1,t35_finseq_1,t29_nat_1,t38_nat_1,t35_finseq_1,t29_nat_1,t38_nat_1,t46_finseq_1,t29_nat_1,t38_nat_1,d20_qc_lang1,t45_finseq_1,t58_finseq_1,t7_mcart_1,t36_qc_lang1,d20_qc_lang1,t45_finseq_1,t45_finseq_1,t46_finseq_1,t45_finseq_1,t58_finseq_1,t58_finseq_1,t46_finseq_1,t35_finseq_1,t57_finseq_1,t35_finseq_1,t57_finseq_1,t38_nat_1,t38_nat_1,t33_qc_lang1,s4_nat_1]),
    [file(qc_lang1,t37_qc_lang1),interesting(0.90)]).

fof(t47_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ~ ( v5_qc_lang1(A)
          & r1_xreal_0(k3_finseq_1(k10_qc_lang1(A)),k3_finseq_1(k10_qc_lang1(k21_qc_lang1(A)))) ) ) ),
    inference(mizar_proof,[status(thm)],[d20_qc_lang1,t45_finseq_1,t35_finseq_1,t57_finseq_1,t35_finseq_1,t29_nat_1,t38_nat_1,d27_qc_lang1]),
    [file(qc_lang1,t47_qc_lang1),interesting(0.79)]).

fof(t4_qc_lang1,theorem,(
    r1_tarski(k1_qc_lang1,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers)) ),
    inference(mizar_proof,[status(thm)],[t2_qc_lang1]),
    [file(qc_lang1,t4_qc_lang1),interesting(0.76)]).

fof(t10_qc_lang1,theorem,(
    r1_tarski(k5_qc_lang1,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers)) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d2_zfmisc_1]),
    [file(qc_lang1,t10_qc_lang1),interesting(0.75)]).

fof(t2_qc_lang1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B,C] : 
          ( m1_subset_1(C,A)
         => ! [D] : 
              ( m1_subset_1(D,A)
             => ! [E] : 
                  ( m1_subset_1(E,A)
                 => r1_tarski(k2_zfmisc_1(k1_enumset1(C,D,E),B),k2_zfmisc_1(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_subset_1,t118_zfmisc_1]),
    [file(qc_lang1,t2_qc_lang1),interesting(0.73)]).

fof(t45_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ~ ( v3_qc_lang1(A)
          & r1_xreal_0(k3_finseq_1(k10_qc_lang1(A)),k3_finseq_1(k10_qc_lang1(k17_qc_lang1(A)))) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_qc_lang1,t35_finseq_1,t57_finseq_1,t38_nat_1,d23_qc_lang1]),
    [file(qc_lang1,t45_qc_lang1),interesting(0.73)]).

fof(t21_qc_lang1,theorem,(
    v1_qc_lang1(k8_qc_lang1) ),
    inference(mizar_proof,[status(thm)],[d10_qc_lang1]),
    [file(qc_lang1,t21_qc_lang1),interesting(0.72)]).

fof(t46_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v4_qc_lang1(A)
       => ( ~ r1_xreal_0(k3_finseq_1(k10_qc_lang1(A)),k3_finseq_1(k10_qc_lang1(k18_qc_lang1(A))))
          & ~ r1_xreal_0(k3_finseq_1(k10_qc_lang1(A)),k3_finseq_1(k10_qc_lang1(k19_qc_lang1(A)))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d19_qc_lang1,t45_finseq_1,t35_finseq_1,t57_finseq_1,t35_finseq_1,t29_nat_1,t38_nat_1,d24_qc_lang1,d25_qc_lang1]),
    [file(qc_lang1,t46_qc_lang1),interesting(0.69)]).

fof(t1_qc_lang1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B,C] : 
          ( m1_subset_1(C,A)
         => r1_tarski(k2_zfmisc_1(k1_tarski(C),B),k2_zfmisc_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_subset_1,t118_zfmisc_1]),
    [file(qc_lang1,t1_qc_lang1),interesting(0.63)]).

fof(l20_qc_lang1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => m2_finseq_1(k9_finseq_1(k4_tarski(A,B)),k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers)) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_zfmisc_1,t56_finseq_1,t37_zfmisc_1,d4_finseq_1]),
    [file(qc_lang1,l20_qc_lang1),interesting(0.61)]).

fof(t51_qc_lang1,theorem,
    ( ~ v2_qc_lang1(k11_qc_lang1)
    & ~ v3_qc_lang1(k11_qc_lang1)
    & ~ v4_qc_lang1(k11_qc_lang1)
    & ~ v5_qc_lang1(k11_qc_lang1)
    & ! [A] : 
        ( m1_subset_1(A,k8_qc_lang1)
       => ( ~ ( v2_qc_lang1(A)
              & v3_qc_lang1(A) )
          & ~ ( v2_qc_lang1(A)
              & v4_qc_lang1(A) )
          & ~ ( v2_qc_lang1(A)
              & v5_qc_lang1(A) )
          & ~ ( v3_qc_lang1(A)
              & v4_qc_lang1(A) )
          & ~ ( v3_qc_lang1(A)
              & v5_qc_lang1(A) )
          & ~ ( v4_qc_lang1(A)
              & v5_qc_lang1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_qc_lang1,t50_qc_lang1,t49_qc_lang1,t50_qc_lang1]),
    [file(qc_lang1,t51_qc_lang1),interesting(0.60)]).

fof(t23_qc_lang1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A))
         => ! [C] : 
              ( m1_qc_lang1(C,A)
             => k9_qc_lang1(B,C) = k7_finseq_1(k12_finseq_1(k7_qc_lang1(A),B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_qc_lang1,d11_qc_lang1]),
    [file(qc_lang1,t23_qc_lang1),interesting(0.56)]).

fof(s2_qc_lang1,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,k8_qc_lang1)
       => ( ( v2_qc_lang1(A)
           => p1_s2_qc_lang1(A) )
          & p1_s2_qc_lang1(k11_qc_lang1)
          & ( ( v3_qc_lang1(A)
              & p1_s2_qc_lang1(k17_qc_lang1(A)) )
           => p1_s2_qc_lang1(A) )
          & ( ( v4_qc_lang1(A)
              & p1_s2_qc_lang1(k18_qc_lang1(A))
              & p1_s2_qc_lang1(k19_qc_lang1(A)) )
           => p1_s2_qc_lang1(A) )
          & ( ( v5_qc_lang1(A)
              & p1_s2_qc_lang1(k21_qc_lang1(A)) )
           => p1_s2_qc_lang1(A) ) ) )
   => ! [A] : 
        ( m1_subset_1(A,k8_qc_lang1)
       => p1_s2_qc_lang1(A) ) ),
    inference(mizar_proof,[status(thm)],[d17_qc_lang1,d18_qc_lang1,d23_qc_lang1,d19_qc_lang1,d24_qc_lang1,d25_qc_lang1,d20_qc_lang1,d27_qc_lang1,s1_qc_lang1]),
    [file(qc_lang1,s2_qc_lang1),interesting(0.56)]).

fof(l21_qc_lang1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A))
         => ! [C] : 
              ( m1_qc_lang1(C,A)
             => m2_finseq_1(k7_finseq_1(k12_finseq_1(k7_qc_lang1(A),B),C),k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_qc_lang1,t10_qc_lang1,t1_xboole_1,t1_xboole_1,t8_xboole_1,t44_finseq_1,d4_finseq_1]),
    [file(qc_lang1,l21_qc_lang1),interesting(0.46)]).

fof(t48_qc_lang1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A))
         => ( k1_mcart_1(B) != 0
            & k1_mcart_1(B) != 1
            & k1_mcart_1(B) != 2
            & k1_mcart_1(B) != 3 ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_qc_lang1,t29_nat_1]),
    [file(qc_lang1,t48_qc_lang1),interesting(0.44)]).

fof(t50_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v2_qc_lang1(A)
       => ( k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) != 0
          & k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) != 1
          & k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) != 2
          & k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) != 3 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_qc_lang1,t48_qc_lang1]),
    [file(qc_lang1,t50_qc_lang1),interesting(0.43)]).

fof(s1_qc_lang1,theorem,
    ( ( ! [A] : 
          ( m2_subset_1(A,k1_numbers,k5_numbers)
         => ! [B] : 
              ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A))
             => ! [C] : 
                  ( m1_qc_lang1(C,A)
                 => p1_s1_qc_lang1(k9_qc_lang1(B,C)) ) ) )
      & p1_s1_qc_lang1(k11_qc_lang1)
      & ! [A] : 
          ( m1_subset_1(A,k8_qc_lang1)
         => ( p1_s1_qc_lang1(A)
           => p1_s1_qc_lang1(k12_qc_lang1(A)) ) )
      & ! [A] : 
          ( m1_subset_1(A,k8_qc_lang1)
         => ! [B] : 
              ( m1_subset_1(B,k8_qc_lang1)
             => ( ( p1_s1_qc_lang1(A)
                  & p1_s1_qc_lang1(B) )
               => p1_s1_qc_lang1(k13_qc_lang1(A,B)) ) ) )
      & ! [A] : 
          ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1)
         => ! [B] : 
              ( m1_subset_1(B,k8_qc_lang1)
             => ( p1_s1_qc_lang1(B)
               => p1_s1_qc_lang1(k14_qc_lang1(A,B)) ) ) ) )
   => ! [A] : 
        ( m1_subset_1(A,k8_qc_lang1)
       => p1_s1_qc_lang1(A) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d11_finseq_1,d9_qc_lang1,t23_qc_lang1,d10_qc_lang1,d3_tarski]),
    [file(qc_lang1,s1_qc_lang1),interesting(0.28)]).

fof(l22_qc_lang1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1)
     => ! [B] : 
          ( m2_finseq_1(B,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers))
         => m2_finseq_1(k7_finseq_1(k7_finseq_1(k9_finseq_1(k4_tarski(3,0)),k12_finseq_1(k2_qc_lang1,A)),B),k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers)) ) ) ),
    inference(mizar_proof,[status(thm)],[l20_qc_lang1,t4_qc_lang1,t1_xboole_1,t1_xboole_1,d4_finseq_1]),
    [file(qc_lang1,l22_qc_lang1),interesting(0.22)]).

fof(t36_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( ( k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 0
         => A = k11_qc_lang1 )
        & ( k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 1
         => v3_qc_lang1(A) )
        & ( k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 2
         => v4_qc_lang1(A) )
        & ( k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 3
         => v5_qc_lang1(A) )
        & ( ? [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
              & m2_subset_1(k1_funct_1(k10_qc_lang1(A),1),k5_qc_lang1,k7_qc_lang1(B)) )
         => v2_qc_lang1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_qc_lang1,t29_nat_1,d17_qc_lang1,t23_qc_lang1,t58_finseq_1,d8_finseq_1,t7_mcart_1,d18_qc_lang1,t58_finseq_1,t7_mcart_1,d19_qc_lang1,t45_finseq_1,t58_finseq_1,t7_mcart_1,d20_qc_lang1,t45_finseq_1,t58_finseq_1,t7_mcart_1,t33_qc_lang1]),
    [file(qc_lang1,t36_qc_lang1),interesting(0.06)]).

fof(s3_qc_lang1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k8_qc_lang1,f1_s3_qc_lang1)
      & m2_relset_1(A,k8_qc_lang1,f1_s3_qc_lang1)
      & k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k11_qc_lang1) = f2_s3_qc_lang1
      & ! [B] : 
          ( m1_subset_1(B,k8_qc_lang1)
         => ( ( v2_qc_lang1(B)
             => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f3_s3_qc_lang1(B) )
            & ( v3_qc_lang1(B)
             => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f4_s3_qc_lang1(k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k17_qc_lang1(B))) )
            & ( v4_qc_lang1(B)
             => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f5_s3_qc_lang1(k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k18_qc_lang1(B)),k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k19_qc_lang1(B))) )
            & ( v5_qc_lang1(B)
             => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f6_s3_qc_lang1(B,k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k21_qc_lang1(B))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_funcop_1,t13_funcop_1,t34_qc_lang1,t2_xreal_1,t51_qc_lang1,t51_qc_lang1,t51_qc_lang1,t51_qc_lang1,t51_qc_lang1,t33_qc_lang1,s3_funct_2,t26_nat_1,t45_qc_lang1,t26_nat_1,t46_qc_lang1,t46_qc_lang1,t26_nat_1,t47_qc_lang1,t26_nat_1,s1_nat_1,t45_qc_lang1,t2_xreal_1,t46_qc_lang1,t46_qc_lang1,t2_xreal_1,t47_qc_lang1,t2_xreal_1,s2_qc_lang1,s2_funct_1,d3_tarski,d5_funct_1,d1_funct_2,t11_relset_1,t2_xreal_1,t45_qc_lang1,t46_qc_lang1,t46_qc_lang1,t47_qc_lang1]),
    [file(qc_lang1,s3_qc_lang1),interesting(0.04)]).

fof(t57_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,A)
     => ! [C] : 
          ( m1_subset_1(C,A)
         => ! [D] : 
              ( m1_subset_1(D,A)
             => ( A != k1_xboole_0
               => m1_subset_1(k1_enumset1(B,C,D),k1_zfmisc_1(A)) ) ) ) ) ),
    file(subset_1,t57_subset_1),
    [interesting(0.00)]).

fof(t118_zfmisc_1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(A,B)
     => ( r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,C))
        & r1_tarski(k2_zfmisc_1(C,A),k2_zfmisc_1(C,B)) ) ) ),
    file(zfmisc_1,t118_zfmisc_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(d2_zfmisc_1,definition,(
    ! [A,B,C] : 
      ( C = k2_zfmisc_1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E,F] : 
              ( r2_hidden(E,A)
              & r2_hidden(F,B)
              & D = k4_tarski(E,F) ) ) ) ),
    file(zfmisc_1,d2_zfmisc_1),
    [interesting(0.00)]).

fof(t1_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(B,C) )
     => r1_tarski(A,C) ) ),
    file(xboole_1,t1_xboole_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(t44_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => k2_relat_1(k7_finseq_1(A,B)) = k2_xboole_0(k2_relat_1(A),k2_relat_1(B)) ) ) ),
    file(finseq_1,t44_finseq_1),
    [interesting(0.00)]).

fof(d4_finseq_1,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( m1_finseq_1(B,A)
      <=> r1_tarski(k2_relat_1(B),A) ) ) ),
    file(finseq_1,d4_finseq_1),
    [interesting(0.00)]).

fof(t56_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k3_finseq_1(B) = 1
          & k2_relat_1(B) = k1_tarski(A) ) ) ) ),
    file(finseq_1,t56_finseq_1),
    [interesting(0.00)]).

fof(t37_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(k1_tarski(A),B)
    <=> r2_hidden(A,B) ) ),
    file(zfmisc_1,t37_zfmisc_1),
    [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(d17_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v2_qc_lang1(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ? [C] : 
                ( m2_subset_1(C,k5_qc_lang1,k7_qc_lang1(B))
                & ? [D] : 
                    ( m1_qc_lang1(D,B)
                    & A = k9_qc_lang1(C,D) ) ) ) ) ) ),
    file(qc_lang1,d17_qc_lang1),
    [interesting(0.00)]).

fof(d8_qc_lang1,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_finseq_1(B,k1_qc_lang1)
         => ( m1_qc_lang1(B,A)
          <=> k3_finseq_1(B) = A ) ) ) ),
    file(qc_lang1,d8_qc_lang1),
    [interesting(0.00)]).

fof(d11_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k5_qc_lang1)
     => ! [B] : 
          ( m2_finseq_1(B,k1_qc_lang1)
         => ( k6_qc_lang1(A) = k3_finseq_1(B)
           => k9_qc_lang1(A,B) = k7_finseq_1(k12_finseq_1(k5_qc_lang1,A),B) ) ) ) ),
    file(qc_lang1,d11_qc_lang1),
    [interesting(0.00)]).

fof(t35_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ),
    file(finseq_1,t35_finseq_1),
    [interesting(0.00)]).

fof(t29_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ),
    file(nat_1,t29_nat_1),
    [interesting(0.00)]).

fof(d18_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v3_qc_lang1(A)
      <=> ? [B] : 
            ( m1_subset_1(B,k8_qc_lang1)
            & A = k12_qc_lang1(B) ) ) ) ),
    file(qc_lang1,d18_qc_lang1),
    [interesting(0.00)]).

fof(d19_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v4_qc_lang1(A)
      <=> ? [B] : 
            ( m1_subset_1(B,k8_qc_lang1)
            & ? [C] : 
                ( m1_subset_1(C,k8_qc_lang1)
                & A = k13_qc_lang1(B,C) ) ) ) ) ),
    file(qc_lang1,d19_qc_lang1),
    [interesting(0.00)]).

fof(t45_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ),
    file(finseq_1,t45_finseq_1),
    [interesting(0.00)]).

fof(d20_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v5_qc_lang1(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1)
            & ? [C] : 
                ( m1_subset_1(C,k8_qc_lang1)
                & A = k14_qc_lang1(B,C) ) ) ) ) ),
    file(qc_lang1,d20_qc_lang1),
    [interesting(0.00)]).

fof(d11_finseq_1,definition,(
    ! [A,B] : 
      ( B = k13_finseq_1(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> m2_finseq_1(C,A) ) ) ),
    file(finseq_1,d11_finseq_1),
    [interesting(0.00)]).

fof(d9_qc_lang1,definition,(
    ! [A] : 
      ( v1_qc_lang1(A)
    <=> ( m1_subset_1(A,k1_zfmisc_1(k13_finseq_1(k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers))))
        & ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ! [C] : 
                ( m2_subset_1(C,k5_qc_lang1,k7_qc_lang1(B))
               => ! [D] : 
                    ( m1_qc_lang1(D,B)
                   => r2_hidden(k7_finseq_1(k12_finseq_1(k7_qc_lang1(B),C),D),A) ) ) )
        & r2_hidden(k9_finseq_1(k4_tarski(0,0)),A)
        & ! [B] : 
            ( m2_finseq_1(B,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers))
           => ( r2_hidden(B,A)
             => r2_hidden(k7_finseq_1(k9_finseq_1(k4_tarski(1,0)),B),A) ) )
        & ! [B] : 
            ( m2_finseq_1(B,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers))
           => ! [C] : 
                ( m2_finseq_1(C,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers))
               => ( ( r2_hidden(B,A)
                    & r2_hidden(C,A) )
                 => r2_hidden(k7_finseq_1(k7_finseq_1(k9_finseq_1(k4_tarski(2,0)),B),C),A) ) ) )
        & ! [B] : 
            ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1)
           => ! [C] : 
                ( m2_finseq_1(C,k12_mcart_1(k1_numbers,k1_numbers,k5_numbers,k5_numbers))
               => ( r2_hidden(C,A)
                 => r2_hidden(k7_finseq_1(k7_finseq_1(k9_finseq_1(k4_tarski(3,0)),k12_finseq_1(k2_qc_lang1,B)),C),A) ) ) ) ) ) ),
    file(qc_lang1,d9_qc_lang1),
    [interesting(0.00)]).

fof(d10_qc_lang1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( A = k8_qc_lang1
      <=> ( v1_qc_lang1(A)
          & ! [B] : 
              ( ~ v1_xboole_0(B)
             => ( v1_qc_lang1(B)
               => r1_tarski(A,B) ) ) ) ) ) ),
    file(qc_lang1,d10_qc_lang1),
    [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(d8_finseq_1,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k1_relat_1(B) = k2_finseq_1(1)
          & k1_funct_1(B,1) = A ) ) ) ),
    file(finseq_1,d8_finseq_1),
    [interesting(0.00)]).

fof(t7_mcart_1,theorem,(
    ! [A,B] : 
      ( k1_mcart_1(k4_tarski(A,B)) = A
      & k2_mcart_1(k4_tarski(A,B)) = B ) ),
    file(mcart_1,t7_mcart_1),
    [interesting(0.00)]).

fof(t58_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k1_funct_1(k7_finseq_1(k9_finseq_1(A),B),1) = A ) ),
    file(finseq_1,t58_finseq_1),
    [interesting(0.00)]).

fof(t49_qc_lang1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( k1_mcart_1(k1_funct_1(k10_qc_lang1(k11_qc_lang1),1)) = 0
        & ~ ( v2_qc_lang1(A)
            & ! [B] : 
                ( m2_subset_1(B,k1_numbers,k5_numbers)
               => ~ m2_subset_1(k1_funct_1(k10_qc_lang1(A),1),k5_qc_lang1,k7_qc_lang1(B)) ) )
        & ( v3_qc_lang1(A)
         => k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 1 )
        & ( v4_qc_lang1(A)
         => k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 2 )
        & ( v5_qc_lang1(A)
         => k1_mcart_1(k1_funct_1(k10_qc_lang1(A),1)) = 3 ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_finseq_1,t7_mcart_1,d17_qc_lang1,t23_qc_lang1,t58_finseq_1,d18_qc_lang1,t58_finseq_1,t7_mcart_1,d19_qc_lang1,t45_finseq_1,t58_finseq_1,t7_mcart_1,d20_qc_lang1,t45_finseq_1,t58_finseq_1,t7_mcart_1]),
    [file(qc_lang1,t49_qc_lang1),interesting(0.00)]).

fof(d6_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k5_qc_lang1)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( B = k6_qc_lang1(A)
          <=> k1_mcart_1(A) = k1_nat_1(7,B) ) ) ) ),
    file(qc_lang1,d6_qc_lang1),
    [interesting(0.00)]).

fof(s3_funct_2,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s3_funct_2)
       => ? [B] : 
            ( m1_subset_1(B,f2_s3_funct_2)
            & p1_s3_funct_2(A,B) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,f1_s3_funct_2,f2_s3_funct_2)
        & m2_relset_1(A,f1_s3_funct_2,f2_s3_funct_2)
        & ! [B] : 
            ( m1_subset_1(B,f1_s3_funct_2)
           => p1_s3_funct_2(B,k8_funct_2(f1_s3_funct_2,f2_s3_funct_2,A,B)) ) ) ),
    file(funct_2,s3_funct_2),
    [interesting(0.00)]).

fof(t26_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ~ ( r1_xreal_0(A,k2_xcmplx_0(B,1))
              & ~ r1_xreal_0(A,B)
              & A != k2_xcmplx_0(B,1) ) ) ) ),
    file(nat_1,t26_nat_1),
    [interesting(0.00)]).

fof(t57_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k3_finseq_1(B) = 1
          & k1_funct_1(B,1) = A ) ) ) ),
    file(finseq_1,t57_finseq_1),
    [interesting(0.00)]).

fof(t38_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A)
          <=> r1_xreal_0(A,B) ) ) ) ),
    file(nat_1,t38_nat_1),
    [interesting(0.00)]).

fof(d23_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v3_qc_lang1(A)
       => ! [B] : 
            ( m1_subset_1(B,k8_qc_lang1)
           => ( B = k17_qc_lang1(A)
            <=> A = k12_qc_lang1(B) ) ) ) ) ),
    file(qc_lang1,d23_qc_lang1),
    [interesting(0.00)]).

fof(d24_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v4_qc_lang1(A)
       => ! [B] : 
            ( m1_subset_1(B,k8_qc_lang1)
           => ( B = k18_qc_lang1(A)
            <=> ? [C] : 
                  ( m1_subset_1(C,k8_qc_lang1)
                  & A = k13_qc_lang1(B,C) ) ) ) ) ) ),
    file(qc_lang1,d24_qc_lang1),
    [interesting(0.00)]).

fof(d25_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v4_qc_lang1(A)
       => ! [B] : 
            ( m1_subset_1(B,k8_qc_lang1)
           => ( B = k19_qc_lang1(A)
            <=> ? [C] : 
                  ( m1_subset_1(C,k8_qc_lang1)
                  & A = k13_qc_lang1(C,B) ) ) ) ) ) ),
    file(qc_lang1,d25_qc_lang1),
    [interesting(0.00)]).

fof(d27_qc_lang1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k8_qc_lang1)
     => ( v5_qc_lang1(A)
       => ! [B] : 
            ( m1_subset_1(B,k8_qc_lang1)
           => ( B = k21_qc_lang1(A)
            <=> ? [C] : 
                  ( m2_subset_1(C,k1_qc_lang1,k2_qc_lang1)
                  & A = k14_qc_lang1(C,B) ) ) ) ) ) ),
    file(qc_lang1,d27_qc_lang1),
    [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(s2_funct_1,theorem,
    ( ( ! [A,B,C] : 
          ( ( r2_hidden(A,f1_s2_funct_1)
            & p1_s2_funct_1(A,B)
            & p1_s2_funct_1(A,C) )
         => B = C )
      & ! [A] : ~ ( r2_hidden(A,f1_s2_funct_1)
          & ! [B] : ~ p1_s2_funct_1(A,B) ) )
   => ? [A] : 
        ( v1_relat_1(A)
        & v1_funct_1(A)
        & k1_relat_1(A) = f1_s2_funct_1
        & ! [B] : 
            ( r2_hidden(B,f1_s2_funct_1)
           => p1_s2_funct_1(B,k1_funct_1(A,B)) ) ) ),
    file(funct_1,s2_funct_1),
    [interesting(0.00)]).

fof(d5_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : 
                  ( r2_hidden(D,k1_relat_1(A))
                  & C = k1_funct_1(A,D) ) ) ) ) ),
    file(funct_1,d5_funct_1),
    [interesting(0.00)]).

fof(d1_funct_2,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( ( ( B = k1_xboole_0
           => A = k1_xboole_0 )
         => ( v1_funct_2(C,A,B)
          <=> A = k4_relset_1(A,B,C) ) )
        & ( B = k1_xboole_0
         => ( A = k1_xboole_0
            | ( v1_funct_2(C,A,B)
            <=> C = k1_xboole_0 ) ) ) ) ) ),
    file(funct_2,d1_funct_2),
    [interesting(0.00)]).

fof(t11_relset_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => m2_relset_1(C,A,B) ) ) ),
    file(relset_1,t11_relset_1),
    [interesting(0.00)]).

fof(t11_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t11_qc_lang1),
    [interesting(0.00)]).

fof(t12_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t12_qc_lang1),
    [interesting(0.00)]).

fof(t13_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t13_qc_lang1),
    [interesting(0.00)]).

fof(t14_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t14_qc_lang1),
    [interesting(0.00)]).

fof(t15_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t15_qc_lang1),
    [interesting(0.00)]).

fof(t16_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t16_qc_lang1),
    [interesting(0.00)]).

fof(t17_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t17_qc_lang1),
    [interesting(0.00)]).

fof(t18_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t18_qc_lang1),
    [interesting(0.00)]).

fof(t19_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t19_qc_lang1),
    [interesting(0.00)]).

fof(t63_subset_1,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => m1_subset_1(k1_tarski(A),k1_zfmisc_1(B)) ) ),
    file(subset_1,t63_subset_1),
    [interesting(0.00)]).

fof(t20_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t20_qc_lang1),
    [interesting(0.00)]).

fof(t22_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t22_qc_lang1),
    [interesting(0.00)]).

fof(t24_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t24_qc_lang1),
    [interesting(0.00)]).

fof(t25_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t25_qc_lang1),
    [interesting(0.00)]).

fof(t26_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t26_qc_lang1),
    [interesting(0.00)]).

fof(t27_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t27_qc_lang1),
    [interesting(0.00)]).

fof(t28_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t28_qc_lang1),
    [interesting(0.00)]).

fof(t29_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t29_qc_lang1),
    [interesting(0.00)]).

fof(t30_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t30_qc_lang1),
    [interesting(0.00)]).

fof(t31_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t31_qc_lang1),
    [interesting(0.00)]).

fof(t32_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t32_qc_lang1),
    [interesting(0.00)]).

fof(d3_finseq_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( B = k3_finseq_1(A)
          <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ),
    file(finseq_1,d3_finseq_1),
    [interesting(0.00)]).

fof(t3_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r2_hidden(A,k2_finseq_1(B))
          <=> ( r1_xreal_0(1,A)
              & r1_xreal_0(A,B) ) ) ) ) ),
    file(finseq_1,t3_finseq_1),
    [interesting(0.00)]).

fof(d7_finseq_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( C = k7_finseq_1(A,B)
              <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(A))
                       => k1_funct_1(C,D) = k1_funct_1(A,D) ) )
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(B))
                       => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ),
    file(finseq_1,d7_finseq_1),
    [interesting(0.00)]).

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

fof(t25_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k3_finseq_1(A) = 0
      <=> A = k1_xboole_0 ) ) ),
    file(finseq_1,t25_finseq_1),
    [interesting(0.00)]).

fof(t47_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k7_finseq_1(A,k1_xboole_0) = A
        & k7_finseq_1(k1_xboole_0,A) = A ) ) ),
    file(finseq_1,t47_finseq_1),
    [interesting(0.00)]).

fof(t35_qc_lang1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A))
         => k6_qc_lang1(B) = A ) ) ),
    file(qc_lang1,t35_qc_lang1),
    [interesting(0.00)]).

fof(t46_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( k7_finseq_1(A,B) = k7_finseq_1(C,B)
                  | k7_finseq_1(B,A) = k7_finseq_1(B,C) )
               => A = C ) ) ) ) ),
    file(finseq_1,t46_finseq_1),
    [interesting(0.00)]).

fof(t64_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ! [D] : 
                  ( ( v1_relat_1(D)
                    & v1_funct_1(D)
                    & v1_finseq_1(D) )
                 => ~ ( k7_finseq_1(A,B) = k7_finseq_1(C,D)
                      & r1_xreal_0(k3_finseq_1(A),k3_finseq_1(C))
                      & ! [E] : 
                          ( ( v1_relat_1(E)
                            & v1_funct_1(E)
                            & v1_finseq_1(E) )
                         => k7_finseq_1(A,E) != C ) ) ) ) ) ) ),
    file(finseq_1,t64_finseq_1),
    [interesting(0.00)]).

fof(s4_nat_1,theorem,
    ( ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(A,B)
               => p1_s4_nat_1(B) ) )
         => p1_s4_nat_1(A) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => p1_s4_nat_1(A) ) ),
    file(nat_1,s4_nat_1),
    [interesting(0.00)]).

fof(t38_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t38_qc_lang1),
    [interesting(0.00)]).

fof(t39_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t39_qc_lang1),
    [interesting(0.00)]).

fof(t3_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t3_qc_lang1),
    [interesting(0.00)]).

fof(t40_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t40_qc_lang1),
    [interesting(0.00)]).

fof(t41_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t41_qc_lang1),
    [interesting(0.00)]).

fof(t42_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t42_qc_lang1),
    [interesting(0.00)]).

fof(t43_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t43_qc_lang1),
    [interesting(0.00)]).

fof(t44_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t44_qc_lang1),
    [interesting(0.00)]).

fof(t5_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t5_qc_lang1),
    [interesting(0.00)]).

fof(t6_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t6_qc_lang1),
    [interesting(0.00)]).

fof(t7_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t7_qc_lang1),
    [interesting(0.00)]).

fof(t8_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t8_qc_lang1),
    [interesting(0.00)]).

fof(t9_qc_lang1,theorem,(
    $true ),
    file(qc_lang1,t9_qc_lang1),
    [interesting(0.00)]).