fof(t54_ami_6,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k5_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A) = k16_ami_3(A) ) ),
    inference(mizar_proof,[status(thm)],[s4_funct_2,t53_ami_6,t53_ami_6,t53_ami_6,t18_amistd_1,d21_ordinal2,d12_amistd_1]),
    [file(ami_6,t54_ami_6),interesting(1.00)]).

fof(t55_ami_6,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k11_ami_3(k5_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A)) = k5_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k2_xcmplx_0(A,1)) ) ),
    inference(mizar_proof,[status(thm)],[t54_ami_6,t54_ami_3,t54_ami_6]),
    [file(ami_6,t55_ami_6),interesting(0.97)]).

fof(t56_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k11_ami_3(A) = k9_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A) ) ),
    inference(mizar_proof,[status(thm)],[t55_ami_6,d13_amistd_1]),
    [file(ami_6,t56_ami_6),interesting(0.96)]).

fof(t52_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k3_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A) = k2_struct_0(k1_ami_3,A,k11_ami_3(A)) ) ),
    inference(mizar_proof,[status(thm)],[d4_tarski,t40_ami_6,t71_ami_3,d1_tarski,d2_tarski,t41_ami_6,d1_tarski,d2_tarski,t42_ami_6,d1_tarski,d2_tarski,t43_ami_6,d1_tarski,d2_tarski,t44_ami_6,d1_tarski,d2_tarski,t45_ami_6,d1_tarski,d2_tarski,t46_ami_6,t47_ami_6,t37_xboole_1,t49_ami_6,d4_xboole_0,t48_ami_6,d2_tarski,d1_tarski,d2_tarski,t51_ami_6,d4_xboole_0,t50_ami_6,d2_tarski,d1_tarski,d2_tarski,t69_ami_3,t40_ami_6,d1_tarski,d4_tarski,t42_ami_6,d1_tarski,d4_tarski,d2_tarski,t2_tarski]),
    [file(ami_6,t52_ami_6),interesting(0.75)]).

fof(l7_ami_6,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,k4_finseq_1(k9_finseq_1(B)))
     => A = 1 ) ),
    inference(mizar_proof,[status(thm)],[d8_finseq_1,t4_finseq_1,d1_tarski]),
    [file(ami_6,l7_ami_6),interesting(0.71)]).

fof(l8_ami_6,theorem,(
    ! [A,B,C] : ~ ( r2_hidden(A,k4_finseq_1(k10_finseq_1(B,C)))
      & A != 1
      & A != 2 ) ),
    inference(mizar_proof,[status(thm)],[t29_finseq_3,t4_finseq_1,d2_tarski]),
    [file(ami_6,l8_ami_6),interesting(0.68)]).

fof(t2_ami_6,theorem,(
    k2_ami_2 != u2_ami_1(k1_tarski(k4_numbers),k1_ami_3) ),
    inference(mizar_proof,[status(thm)],[t12_ami_2,d1_ami_3]),
    [file(ami_6,t2_ami_6),interesting(0.67)]).

fof(t7_ami_6,theorem,(
    k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k5_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k1_xboole_0 ),
    inference(mizar_proof,[status(thm)],[t71_ami_3,d2_mcart_1]),
    [file(ami_6,t7_ami_6),interesting(0.63)]).

fof(t8_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B)) = k10_finseq_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_ami_3,d2_mcart_1]),
    [file(ami_6,t8_ami_6),interesting(0.63)]).

fof(t9_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B)) = k10_finseq_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_ami_3,d2_mcart_1]),
    [file(ami_6,t9_ami_6),interesting(0.63)]).

fof(t10_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B)) = k10_finseq_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_ami_3,d2_mcart_1]),
    [file(ami_6,t10_ami_6),interesting(0.63)]).

fof(t11_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B)) = k10_finseq_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_ami_3,d2_mcart_1]),
    [file(ami_6,t11_ami_6),interesting(0.63)]).

fof(t12_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B)) = k10_finseq_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_ami_3,d2_mcart_1]),
    [file(ami_6,t12_ami_6),interesting(0.63)]).

fof(t47_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k2_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(A)) = k1_struct_0(k1_ami_3,A) ) ),
    inference(mizar_proof,[status(thm)],[d1_setfam_1,t46_ami_6,d1_tarski,t46_ami_6,d1_tarski,d1_setfam_1,t2_tarski]),
    [file(ami_6,t47_ami_6),interesting(0.62)]).

fof(t49_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k2_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(B,A)) = k1_struct_0(k1_ami_3,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_setfam_1,t48_ami_6,d2_tarski,t53_ami_3,t4_ami_6,d1_tarski,d1_tarski,t48_ami_6,d2_tarski,d1_setfam_1,t2_tarski]),
    [file(ami_6,t49_ami_6),interesting(0.62)]).

fof(t51_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k2_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(B,A)) = k1_struct_0(k1_ami_3,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_setfam_1,t50_ami_6,d2_tarski,t53_ami_3,t4_ami_6,d1_tarski,d1_tarski,t50_ami_6,d2_tarski,d1_setfam_1,t2_tarski]),
    [file(ami_6,t51_ami_6),interesting(0.61)]).

fof(t45_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k7_ami_3(A,B)) = k1_struct_0(k1_ami_3,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_ami_3,l43_ami_6]),
    [file(ami_6,t45_ami_6),interesting(0.58)]).

fof(t41_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k3_ami_3(A,B)) = k1_struct_0(k1_ami_3,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_ami_3,l43_ami_6]),
    [file(ami_6,t41_ami_6),interesting(0.57)]).

fof(t42_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k4_ami_3(A,B)) = k1_struct_0(k1_ami_3,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_ami_3,l43_ami_6]),
    [file(ami_6,t42_ami_6),interesting(0.57)]).

fof(t43_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k5_ami_3(A,B)) = k1_struct_0(k1_ami_3,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_ami_3,l43_ami_6]),
    [file(ami_6,t43_ami_6),interesting(0.57)]).

fof(t44_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k6_ami_3(A,B)) = k1_struct_0(k1_ami_3,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_ami_3,l43_ami_6]),
    [file(ami_6,t44_ami_6),interesting(0.57)]).

fof(t14_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(B,A)) = k10_finseq_1(B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_ami_3,d2_mcart_1]),
    [file(ami_6,t14_ami_6),interesting(0.56)]).

fof(t15_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(B,A)) = k10_finseq_1(B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_ami_3,d2_mcart_1]),
    [file(ami_6,t15_ami_6),interesting(0.56)]).

fof(t1_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ~ r2_hidden(A,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) ) ),
    inference(mizar_proof,[status(thm)],[d2_ami_3,d1_ami_3,t33_ami_5,t3_xboole_0]),
    [file(ami_6,t1_ami_6),interesting(0.55)]).

fof(t17_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 1
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_ami_6,t38_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t47_ami_5,t8_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t17_ami_6),interesting(0.52)]).

fof(t18_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 2
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_ami_6,t39_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t48_ami_5,t9_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t18_ami_6),interesting(0.52)]).

fof(t16_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 0
       => k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A) = k1_tarski(0) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_ami_5,t7_ami_6,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t7_ami_6,t37_ami_5]),
    [file(ami_6,t16_ami_6),interesting(0.51)]).

fof(t23_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 7
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_ami_6,t44_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t53_ami_5,t14_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t23_ami_6),interesting(0.50)]).

fof(t24_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 8
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_ami_6,t45_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t54_ami_5,t15_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t24_ami_6),interesting(0.50)]).

fof(t19_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 3
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_ami_6,t40_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t49_ami_5,t10_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t19_ami_6),interesting(0.49)]).

fof(t20_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 4
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_ami_6,t41_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t50_ami_5,t11_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t20_ami_6),interesting(0.49)]).

fof(t21_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 5
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k2_tarski(1,2) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_ami_6,t42_ami_5,d1_amistd_2,t4_finseq_1,t29_finseq_3,d3_tarski,d10_xboole_0,d3_tarski,t51_ami_5,t12_ami_6,t4_finseq_1,t29_finseq_3,d1_amistd_2]),
    [file(ami_6,t21_ami_6),interesting(0.49)]).

fof(t36_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(B,A)))),1) = u2_ami_1(k1_tarski(k4_numbers),k1_ami_3) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_ami_5,t23_ami_6,d2_tarski,t44_ami_5,t8_amistd_2,d6_card_3,t53_ami_5,t14_ami_6,t61_finseq_1,d3_tarski,d10_xboole_0,d3_tarski,t14_ami_6,t44_ami_5,t61_finseq_1,d6_card_3,t8_amistd_2]),
    [file(ami_6,t36_ami_6),interesting(0.48)]).

fof(t38_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(B,A)))),1) = u2_ami_1(k1_tarski(k4_numbers),k1_ami_3) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_ami_5,t24_ami_6,d2_tarski,t45_ami_5,t8_amistd_2,d6_card_3,t54_ami_5,t15_ami_6,t61_finseq_1,d3_tarski,d10_xboole_0,d3_tarski,t15_ami_6,t45_ami_5,t61_finseq_1,d6_card_3,t8_amistd_2]),
    [file(ami_6,t38_ami_6),interesting(0.48)]).

fof(t37_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(B,A)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t44_ami_5,t23_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t44_ami_5,t53_ami_5,t14_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t44_ami_5,d6_card_3,t14_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t37_ami_6),interesting(0.47)]).

fof(t39_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(B,A)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t45_ami_5,t24_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t45_ami_5,t54_ami_5,t15_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t45_ami_5,d6_card_3,t15_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t39_ami_6),interesting(0.47)]).

fof(t3_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k1_ami_3))
     => ~ ( A != k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)
          & ~ r2_hidden(A,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
          & ~ m1_ami_3(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_ami_5,d2_xboole_0,d2_xboole_0,d1_ami_3,d2_ami_3,d1_tarski]),
    [file(ami_6,t3_ami_6),interesting(0.44)]).

fof(t25_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B)))),1) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t38_ami_5,t17_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t38_ami_5,t47_ami_5,t8_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t38_ami_5,d6_card_3,t8_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t25_ami_6),interesting(0.42)]).

fof(t26_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t38_ami_5,t17_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t38_ami_5,t47_ami_5,t8_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t38_ami_5,d6_card_3,t8_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t26_ami_6),interesting(0.42)]).

fof(t27_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B)))),1) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t39_ami_5,t18_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t39_ami_5,t48_ami_5,t9_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t39_ami_5,d6_card_3,t9_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t27_ami_6),interesting(0.42)]).

fof(t28_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t39_ami_5,t18_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t39_ami_5,t48_ami_5,t9_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t39_ami_5,d6_card_3,t9_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t28_ami_6),interesting(0.42)]).

fof(t29_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B)))),1) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t40_ami_5,t19_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t40_ami_5,t49_ami_5,t10_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t40_ami_5,d6_card_3,t10_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t29_ami_6),interesting(0.42)]).

fof(t30_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t40_ami_5,t19_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t40_ami_5,t49_ami_5,t10_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t40_ami_5,d6_card_3,t10_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t30_ami_6),interesting(0.42)]).

fof(t31_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B)))),1) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t41_ami_5,t20_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t41_ami_5,t50_ami_5,t11_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t41_ami_5,d6_card_3,t11_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t31_ami_6),interesting(0.42)]).

fof(t32_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t41_ami_5,t20_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t41_ami_5,t50_ami_5,t11_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t41_ami_5,d6_card_3,t11_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t32_ami_6),interesting(0.42)]).

fof(t33_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B)))),1) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t42_ami_5,t21_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t42_ami_5,t51_ami_5,t12_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t42_ami_5,d6_card_3,t12_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t33_ami_6),interesting(0.42)]).

fof(t34_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B)))),2) = k2_ami_2 ) ) ),
    inference(mizar_proof,[status(thm)],[t42_ami_5,t21_ami_6,d2_tarski,d1_amistd_2,d6_card_3,t42_ami_5,t51_ami_5,t12_ami_6,t61_finseq_1,d2_ami_3,d3_tarski,d10_xboole_0,d3_tarski,t16_ami_5,t42_ami_5,d6_card_3,t12_ami_6,t61_finseq_1,d1_amistd_2]),
    [file(ami_6,t34_ami_6),interesting(0.42)]).

fof(t57_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( v4_ordinal2(B)
         => k8_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(A),B) = k8_ami_3(k5_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k2_xcmplx_0(k7_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A),B))) ) ) ),
    inference(mizar_proof,[status(thm)],[d14_amistd_2,t43_ami_5,t43_ami_5,d14_amistd_2,t13_ami_6,d8_finseq_1,d8_finseq_1,t13_ami_6,t13_ami_6,l7_ami_6,t35_ami_6,d14_amistd_2,t13_ami_6,d8_finseq_1,d8_finseq_1,t13_ami_6,t9_funct_1,t16_amistd_2]),
    [file(ami_6,t57_ami_6),interesting(0.39)]).

fof(t58_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ! [C] : 
              ( v4_ordinal2(C)
             => k8_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(B,A),C) = k9_ami_3(k5_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k2_xcmplx_0(k7_amistd_1(k1_tarski(k4_numbers),k1_ami_3,B),C)),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d14_amistd_2,t44_ami_5,t44_ami_5,d14_amistd_2,t14_ami_6,t29_finseq_3,t29_finseq_3,t14_ami_6,t14_ami_6,t36_ami_6,d14_amistd_2,t14_ami_6,t61_finseq_1,t61_finseq_1,t14_ami_6,t2_ami_6,t37_ami_6,d14_amistd_2,t14_ami_6,t61_finseq_1,t61_finseq_1,t14_ami_6,l8_ami_6,t9_funct_1,t16_amistd_2]),
    [file(ami_6,t58_ami_6),interesting(0.36)]).

fof(t59_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ! [C] : 
              ( v4_ordinal2(C)
             => k8_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(B,A),C) = k10_ami_3(k5_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k2_xcmplx_0(k7_amistd_1(k1_tarski(k4_numbers),k1_ami_3,B),C)),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d14_amistd_2,t45_ami_5,t45_ami_5,d14_amistd_2,t15_ami_6,t29_finseq_3,t29_finseq_3,t15_ami_6,t15_ami_6,t38_ami_6,d14_amistd_2,t15_ami_6,t61_finseq_1,t61_finseq_1,t15_ami_6,t2_ami_6,t39_ami_6,d14_amistd_2,t15_ami_6,t61_finseq_1,t61_finseq_1,t15_ami_6,l8_ami_6,t9_funct_1,t16_amistd_2]),
    [file(ami_6,t59_ami_6),interesting(0.36)]).

fof(l9_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( A != 0
          & A != 1
          & A != 2
          & A != 3
          & A != 4
          & A != 5
          & A != 6
          & A != 7
          & A != 8 ) ) ),
    inference(mizar_proof,[status(thm)],[d1_ami_3,d1_ami_3,t10_gr_cy_1,t38_nat_1,t9_cqc_the1]),
    [file(ami_6,l9_ami_6),interesting(0.24)]).

fof(t53_ami_6,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
        & m2_relset_1(A,k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k8_funct_2(k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A,B) = k16_ami_3(B) )
       => ( v3_funct_2(A,k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A,k1_nat_1(B,1)),k3_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k8_funct_2(k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A,B)))
                & ! [C] : 
                    ( m2_subset_1(C,k1_numbers,k5_numbers)
                   => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A,C),k3_amistd_1(k1_tarski(k4_numbers),k1_ami_3,k8_funct_2(k5_numbers,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A,B)))
                     => r1_xreal_0(B,C) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_funct_1,d1_funct_2,t53_ami_3,d4_funct_2,t12_relset_1,d3_funct_2,d10_xboole_0,d3_tarski,t19_ami_5,d1_funct_2,d5_funct_1,t52_ami_6,t54_ami_3,d2_tarski,d4_funct_2,d1_funct_2,d8_funct_1,d8_funct_1,t29_nat_1,d2_tarski]),
    [file(ami_6,t53_ami_6),interesting(0.17)]).

fof(l44_ami_6,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( ! [B] : 
            ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
           => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,B,A) = k1_struct_0(k1_ami_3,k11_ami_3(B)) )
       => v1_xboole_0(k2_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_yellow_8,d1_xboole_0,d1_setfam_1,d1_tarski,t4_ami_6]),
    [file(ami_6,l44_ami_6),interesting(0.10)]).

fof(t6_ami_6,theorem,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & v10_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B)))
             => ! [D] : 
                  ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B)))
                 => ! [E] : 
                      ( m1_struct_0(E,B,u2_ami_1(A,B))
                     => ! [F] : 
                          ( m1_subset_1(F,k3_ami_1(A,B,k2_ami_1(A,B)))
                         => ! [G] : 
                              ( m1_subset_1(G,k3_ami_1(A,B,E))
                             => ( ( F = E
                                  & D = k8_ami_5(A,B,C,k16_ami_1(A,B,k2_ami_1(A,B),E,F,G)) )
                               => ( k13_ami_1(A,B,D,E) = G
                                  & k6_ami_1(A,B,D) = E
                                  & k6_ami_1(A,B,k9_ami_1(A,B,D)) = k1_funct_1(k4_ami_1(A,B,k13_ami_1(A,B,D,k6_ami_1(A,B,D)),D),k2_ami_1(A,B)) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_funct_4,d2_tarski,t48_ami_1,d2_tarski,t14_funct_4,t66_funct_4,d15_ami_1,t14_funct_4,t66_funct_4,d18_ami_1,d17_ami_1,d15_ami_1]),
    [file(ami_6,t6_ami_6),interesting(0.08)]).

fof(d1_yellow_8,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( v1_realset1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,A)
           => ! [C] : 
                ( m1_subset_1(C,A)
               => B = C ) ) ) ) ),
    file(yellow_8,d1_yellow_8),
    [interesting(0.00)]).

fof(d1_xboole_0,definition,(
    ! [A] : 
      ( A = k1_xboole_0
    <=> ! [B] : ~ r2_hidden(B,A) ) ),
    file(xboole_0,d1_xboole_0),
    [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(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [interesting(0.00)]).

fof(d11_ami_3,definition,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ( B = k11_ami_3(A)
          <=> ? [C] : 
                ( m2_subset_1(C,k5_numbers,k3_ami_2)
                & C = A
                & B = k15_ami_2(C) ) ) ) ) ),
    file(ami_3,d11_ami_3),
    [interesting(0.00)]).

fof(d15_ami_2,definition,(
    ! [A] : 
      ( m2_subset_1(A,k5_numbers,k3_ami_2)
     => k15_ami_2(A) = k1_nat_1(A,2) ) ),
    file(ami_2,d15_ami_2),
    [interesting(0.00)]).

fof(t2_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k2_xcmplx_0(A,B) = k2_xcmplx_0(C,B)
               => A = C ) ) ) ) ),
    file(xcmplx_1,t2_xcmplx_1),
    [interesting(0.00)]).

fof(t4_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ~ ( A != B
              & k11_ami_3(A) = k11_ami_3(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_ami_3,d11_ami_3,d15_ami_2,t2_xcmplx_1]),
    [file(ami_6,t4_ami_6),interesting(0.00)]).

fof(d1_ami_3,definition,(
    k1_ami_3 = g1_ami_1(k1_tarski(k4_numbers),k5_numbers,0,k3_ami_2,k1_gr_cy_1(9),k4_ami_2,k5_ami_2,k17_ami_2) ),
    file(ami_3,d1_ami_3),
    [interesting(0.00)]).

fof(t10_gr_cy_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(A,0)
           => ( r2_hidden(B,k1_gr_cy_1(A))
            <=> ~ r1_xreal_0(A,B) ) ) ) ) ),
    file(gr_cy_1,t10_gr_cy_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(t9_cqc_the1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ~ ( r1_xreal_0(A,8)
          & A != 0
          & A != 1
          & A != 2
          & A != 3
          & A != 4
          & A != 5
          & A != 6
          & A != 7
          & A != 8 ) ) ),
    file(cqc_the1,t9_cqc_the1),
    [interesting(0.00)]).

fof(t46_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 0
       => A = k5_ami_1(k1_tarski(k4_numbers),k1_ami_3) ) ) ),
    file(ami_5,t46_ami_5),
    [interesting(0.00)]).

fof(t71_ami_3,theorem,(
    k5_ami_1(k1_tarski(k4_numbers),k1_ami_3) = k4_tarski(0,k1_xboole_0) ),
    file(ami_3,t71_ami_3),
    [interesting(0.00)]).

fof(d2_mcart_1,definition,(
    ! [A] : 
      ( ? [B,C] : A = k4_tarski(B,C)
     => ! [B] : 
          ( B = k2_mcart_1(A)
        <=> ! [C,D] : 
              ( A = k4_tarski(C,D)
             => B = D ) ) ) ),
    file(mcart_1,d2_mcart_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(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(t37_ami_5,theorem,(
    k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k5_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = 0 ),
    file(ami_5,t37_ami_5),
    [interesting(0.00)]).

fof(t38_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B)) = 1 ) ) ),
    file(ami_5,t38_ami_5),
    [interesting(0.00)]).

fof(d3_ami_3,definition,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k3_ami_3(A,B) = k4_tarski(1,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d3_ami_3),
    [interesting(0.00)]).

fof(d1_amistd_2,definition,(
    ! [A] : 
      ( v1_fraenkel(A)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( ~ v1_xboole_0(A)
             => ( B = k1_amistd_2(A)
              <=> ( ! [C] : 
                      ( r2_hidden(C,k1_relat_1(B))
                    <=> ! [D] : 
                          ( ( v1_relat_1(D)
                            & v1_funct_1(D) )
                         => ( r2_hidden(D,A)
                           => r2_hidden(C,k1_relat_1(D)) ) ) )
                  & ! [C] : 
                      ( r2_hidden(C,k1_relat_1(B))
                     => k1_funct_1(B,C) = k5_card_3(C,A) ) ) ) )
            & ( v1_xboole_0(A)
             => ( B = k1_amistd_2(A)
              <=> B = k1_xboole_0 ) ) ) ) ) ),
    file(amistd_2,d1_amistd_2),
    [interesting(0.00)]).

fof(t4_finseq_1,theorem,
    ( k2_finseq_1(0) = k1_xboole_0
    & k2_finseq_1(1) = k1_tarski(1)
    & k2_finseq_1(2) = k2_tarski(1,2) ),
    file(finseq_1,t4_finseq_1),
    [interesting(0.00)]).

fof(t29_finseq_3,theorem,(
    ! [A,B] : k4_finseq_1(k10_finseq_1(A,B)) = k2_finseq_1(2) ),
    file(finseq_3,t29_finseq_3),
    [interesting(0.00)]).

fof(t47_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 1
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k3_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t47_ami_5),
    [interesting(0.00)]).

fof(d2_tarski,definition,(
    ! [A,B,C] : 
      ( C = k2_tarski(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( D = A
            | D = B ) ) ) ),
    file(tarski,d2_tarski),
    [interesting(0.00)]).

fof(d6_card_3,definition,(
    ! [A,B,C] : 
      ( C = k5_card_3(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E] : 
              ( v1_relat_1(E)
              & v1_funct_1(E)
              & r2_hidden(E,B)
              & D = k1_funct_1(E,A) ) ) ) ),
    file(card_3,d6_card_3),
    [interesting(0.00)]).

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

fof(d2_ami_3,definition,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k1_ami_3))
     => ( m1_ami_3(A)
      <=> r2_hidden(A,k2_ami_2) ) ) ),
    file(ami_3,d2_ami_3),
    [interesting(0.00)]).

fof(t16_ami_5,theorem,(
    ! [A] : 
      ( r2_hidden(A,k2_ami_2)
     => m1_ami_3(A) ) ),
    file(ami_5,t16_ami_5),
    [interesting(0.00)]).

fof(t39_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B)) = 2 ) ) ),
    file(ami_5,t39_ami_5),
    [interesting(0.00)]).

fof(d4_ami_3,definition,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k4_ami_3(A,B) = k4_tarski(2,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d4_ami_3),
    [interesting(0.00)]).

fof(t48_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 2
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k4_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t48_ami_5),
    [interesting(0.00)]).

fof(t40_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B)) = 3 ) ) ),
    file(ami_5,t40_ami_5),
    [interesting(0.00)]).

fof(d5_ami_3,definition,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k5_ami_3(A,B) = k4_tarski(3,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d5_ami_3),
    [interesting(0.00)]).

fof(t49_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 3
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k5_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t49_ami_5),
    [interesting(0.00)]).

fof(t41_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B)) = 4 ) ) ),
    file(ami_5,t41_ami_5),
    [interesting(0.00)]).

fof(d6_ami_3,definition,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k6_ami_3(A,B) = k4_tarski(4,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d6_ami_3),
    [interesting(0.00)]).

fof(t50_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 4
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k6_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t50_ami_5),
    [interesting(0.00)]).

fof(t42_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B)) = 5 ) ) ),
    file(ami_5,t42_ami_5),
    [interesting(0.00)]).

fof(d7_ami_3,definition,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => k7_ami_3(A,B) = k4_tarski(5,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d7_ami_3),
    [interesting(0.00)]).

fof(t51_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 5
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k7_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t51_ami_5),
    [interesting(0.00)]).

fof(t23_ami_5,theorem,(
    u1_struct_0(k1_ami_3) = k2_xboole_0(k2_xboole_0(k1_struct_0(k1_ami_3,k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)),k2_ami_2),k3_ami_2) ),
    file(ami_5,t23_ami_5),
    [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(s4_funct_2,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,f1_s4_funct_2,f2_s4_funct_2)
      & m2_relset_1(A,f1_s4_funct_2,f2_s4_funct_2)
      & ! [B] : 
          ( m1_subset_1(B,f1_s4_funct_2)
         => k8_funct_2(f1_s4_funct_2,f2_s4_funct_2,A,B) = f3_s4_funct_2(B) ) ) ),
    file(funct_2,s4_funct_2),
    [interesting(0.00)]).

fof(d8_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
      <=> ! [B,C] : 
            ( ( r2_hidden(B,k1_relat_1(A))
              & r2_hidden(C,k1_relat_1(A))
              & k1_funct_1(A,B) = k1_funct_1(A,C) )
           => B = C ) ) ) ),
    file(funct_1,d8_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(t53_ami_3,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ~ ( A != B
              & k16_ami_3(A) = k16_ami_3(B) ) ) ) ),
    file(ami_3,t53_ami_3),
    [interesting(0.00)]).

fof(d4_funct_2,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( v3_funct_2(C,A,B)
      <=> ( v2_funct_1(C)
          & v2_funct_2(C,A,B) ) ) ) ),
    file(funct_2,d4_funct_2),
    [interesting(0.00)]).

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

fof(d3_funct_2,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( v2_funct_2(C,A,B)
      <=> k2_relat_1(C) = B ) ) ),
    file(funct_2,d3_funct_2),
    [interesting(0.00)]).

fof(t19_ami_5,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ? [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
          & A = k16_ami_3(B) ) ) ),
    file(ami_5,t19_ami_5),
    [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(d4_tarski,definition,(
    ! [A,B] : 
      ( B = k3_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> ? [D] : 
              ( r2_hidden(C,D)
              & r2_hidden(D,A) ) ) ) ),
    file(tarski,d4_tarski),
    [interesting(0.00)]).

fof(d11_ami_1,definition,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & l1_ami_1(B,A) )
     => ( v5_ami_1(B,A)
      <=> k3_ami_1(A,B,k2_ami_1(A,B)) = u2_ami_1(A,B) ) ) ),
    file(ami_1,d11_ami_1),
    [interesting(0.00)]).

fof(d14_ami_1,definition,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & ~ v2_ami_1(B,A)
        & l1_ami_1(B,A) )
     => ( v8_ami_1(B,A)
      <=> ! [C] : 
            ( m1_struct_0(C,B,u2_ami_1(A,B))
           => k3_ami_1(A,B,C) = u4_ami_1(A,B) ) ) ) ),
    file(ami_1,d14_ami_1),
    [interesting(0.00)]).

fof(t65_funct_4,theorem,(
    ! [A,B,C,D] : 
      ( k1_relat_1(k4_funct_4(A,B,C,D)) = k2_tarski(A,B)
      & r1_tarski(k2_relat_1(k4_funct_4(A,B,C,D)),k2_tarski(C,D)) ) ),
    file(funct_4,t65_funct_4),
    [interesting(0.00)]).

fof(t48_ami_1,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & ~ v2_ami_1(B,A)
        & v5_ami_1(B,A)
        & v8_ami_1(B,A)
        & l1_ami_1(B,A) )
     => ( v10_ami_1(B,A)
       => ! [C] : 
            ( m1_struct_0(C,B,u2_ami_1(A,B))
           => k2_ami_1(A,B) != C ) ) ) ),
    file(ami_1,t48_ami_1),
    [interesting(0.00)]).

fof(t14_funct_4,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(B))
           => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ),
    file(funct_4,t14_funct_4),
    [interesting(0.00)]).

fof(t66_funct_4,theorem,(
    ! [A,B,C,D] : 
      ( A != B
     => ( k1_funct_1(k4_funct_4(A,B,C,D),A) = C
        & k1_funct_1(k4_funct_4(A,B,C,D),B) = D ) ) ),
    file(funct_4,t66_funct_4),
    [interesting(0.00)]).

fof(d15_ami_1,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B)))
             => k6_ami_1(A,B,C) = k1_funct_1(C,k2_ami_1(A,B)) ) ) ) ),
    file(ami_1,d15_ami_1),
    [interesting(0.00)]).

fof(d18_ami_1,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B)))
             => k9_ami_1(A,B,C) = k4_ami_1(A,B,k8_ami_1(A,B,C),C) ) ) ) ),
    file(ami_1,d18_ami_1),
    [interesting(0.00)]).

fof(d17_ami_1,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B)))
             => k8_ami_1(A,B,C) = k1_funct_1(C,k6_ami_1(A,B,C)) ) ) ) ),
    file(ami_1,d17_ami_1),
    [interesting(0.00)]).

fof(d8_ami_1,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v2_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B))
             => ( v3_ami_1(C,A,B)
              <=> ! [D] : 
                    ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B)))
                   => k4_ami_1(A,B,C,D) = D ) ) ) ) ) ),
    file(ami_1,d8_ami_1),
    [interesting(0.00)]).

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

fof(t40_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A,k5_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k1_struct_0(k1_ami_3,A) ) ),
    inference(mizar_proof,[status(thm)],[d11_ami_1,d14_ami_1,t65_funct_4,d2_tarski,t48_ami_1,t6_ami_6,t6_ami_6,t6_ami_6,d8_ami_1,t14_funct_4,t66_funct_4,d18_ami_1,d17_ami_1,d15_ami_1,d8_ami_1,d15_ami_1,d1_tarski,t2_tarski]),
    [file(ami_6,t40_ami_6),interesting(0.00)]).

fof(t8_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C))
                & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B),C),A) = k2_ami_3(C,B)
                & ! [D] : 
                    ( m1_ami_3(D)
                   => ( D != A
                     => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B),C),D) = k2_ami_3(C,D) ) ) ) ) ) ) ),
    file(ami_3,t8_ami_3),
    [interesting(0.00)]).

fof(l43_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ( ! [C] : 
                ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
               => ( ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C) = A
                    & k13_ami_1(k1_tarski(k4_numbers),k1_ami_3,C,A) = B )
                 => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,B,C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C)) ) )
           => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,A,B) = k1_struct_0(k1_ami_3,k11_ami_3(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_ami_1,d18_ami_1,d17_ami_1,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,d11_ami_1,d14_ami_1,t6_ami_6,t6_ami_6,t6_ami_6]),
    [file(ami_6,l43_ami_6),interesting(0.00)]).

fof(t9_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C))
                & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B),C),A) = k2_xcmplx_0(k2_ami_3(C,A),k2_ami_3(C,B))
                & ! [D] : 
                    ( m1_ami_3(D)
                   => ( D != A
                     => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k4_ami_3(A,B),C),D) = k2_ami_3(C,D) ) ) ) ) ) ) ),
    file(ami_3,t9_ami_3),
    [interesting(0.00)]).

fof(t10_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C))
                & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B),C),A) = k6_xcmplx_0(k2_ami_3(C,A),k2_ami_3(C,B))
                & ! [D] : 
                    ( m1_ami_3(D)
                   => ( D != A
                     => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k5_ami_3(A,B),C),D) = k2_ami_3(C,D) ) ) ) ) ) ) ),
    file(ami_3,t10_ami_3),
    [interesting(0.00)]).

fof(t11_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C))
                & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B),C),A) = k3_xcmplx_0(k2_ami_3(C,A),k2_ami_3(C,B))
                & ! [D] : 
                    ( m1_ami_3(D)
                   => ( D != A
                     => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k6_ami_3(A,B),C),D) = k2_ami_3(C,D) ) ) ) ) ) ) ),
    file(ami_3,t11_ami_3),
    [interesting(0.00)]).

fof(t12_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C))
                & ( A != B
                 => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),A) = k5_int_1(k2_ami_3(C,A),k2_ami_3(C,B)) )
                & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),B) = k6_int_1(k2_ami_3(C,A),k2_ami_3(C,B))
                & ! [D] : 
                    ( m1_ami_3(D)
                   => ~ ( D != A
                        & D != B
                        & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),D) != k2_ami_3(C,D) ) ) ) ) ) ) ),
    file(ami_3,t12_ami_3),
    [interesting(0.00)]).

fof(t13_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = B
                & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(B),C),A) = k2_ami_3(C,A) ) ) ) ) ),
    file(ami_3,t13_ami_3),
    [interesting(0.00)]).

fof(t46_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,B,k8_ami_3(A)) = k1_struct_0(k1_ami_3,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_ami_1,d14_ami_1,t6_ami_6,t6_ami_6,t6_ami_6,t13_ami_3,d18_ami_1,d17_ami_1,d15_ami_1,t13_ami_3,d1_tarski,t2_tarski]),
    [file(ami_6,t46_ami_6),interesting(0.00)]).

fof(t37_xboole_1,theorem,(
    ! [A,B] : 
      ( k4_xboole_0(A,B) = k1_xboole_0
    <=> r1_tarski(A,B) ) ),
    file(xboole_1,t37_xboole_1),
    [interesting(0.00)]).

fof(t14_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => ! [D] : 
                  ( m1_subset_1(D,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
                 => ( ( k2_ami_3(D,A) = 0
                     => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(C,A),D),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = C )
                    & ( k2_ami_3(D,A) != 0
                     => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(C,A),D),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,D)) )
                    & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(C,A),D),B) = k2_ami_3(D,B) ) ) ) ) ) ),
    file(ami_3,t14_ami_3),
    [interesting(0.00)]).

fof(t33_ami_5,theorem,(
    r1_subset_1(k2_ami_2,k3_ami_2) ),
    file(ami_5,t33_ami_5),
    [interesting(0.00)]).

fof(t3_xboole_0,theorem,(
    ! [A,B] : 
      ( ~ ( ~ r1_xboole_0(A,B)
          & ! [C] : ~ ( r2_hidden(C,A)
              & r2_hidden(C,B) ) )
      & ~ ( ? [C] : 
              ( r2_hidden(C,A)
              & r2_hidden(C,B) )
          & r1_xboole_0(A,B) ) ) ),
    file(xboole_0,t3_xboole_0),
    [interesting(0.00)]).

fof(t20_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => A != k2_ami_1(k1_tarski(k4_numbers),k1_ami_3) ) ),
    file(ami_5,t20_ami_5),
    [interesting(0.00)]).

fof(t5_cqc_lang,theorem,(
    ! [A,B] : 
      ( k1_relat_1(k3_cqc_lang(A,B)) = k1_tarski(A)
      & k2_relat_1(k3_cqc_lang(A,B)) = k1_tarski(B) ) ),
    file(cqc_lang,t5_cqc_lang),
    [interesting(0.00)]).

fof(t12_funct_4,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( ~ r2_hidden(A,k1_relat_1(B))
           => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(C,A) ) ) ) ),
    file(funct_4,t12_funct_4),
    [interesting(0.00)]).

fof(t6_cqc_lang,theorem,(
    ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ),
    file(cqc_lang,t6_cqc_lang),
    [interesting(0.00)]).

fof(t48_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k9_ami_3(B,A)) = k2_struct_0(k1_ami_3,B,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_ami_1,d17_ami_1,d15_ami_1,t14_ami_3,d2_tarski,t14_ami_3,d2_tarski,d3_tarski,d10_xboole_0,d3_tarski,d11_ami_1,d14_ami_1,t1_ami_6,t20_ami_5,t5_cqc_lang,d1_tarski,d15_ami_1,t12_funct_4,d15_ami_1,t6_ami_6,d1_tarski,t12_funct_4,t6_ami_6,d1_tarski,t14_funct_4,t6_cqc_lang,d18_ami_1,d17_ami_1,d15_ami_1,t14_ami_3,t5_cqc_lang,d1_tarski,d15_ami_1,t12_funct_4,d15_ami_1,t6_ami_6,d1_tarski,t12_funct_4,t6_ami_6,d1_tarski,t14_funct_4,t6_cqc_lang,d18_ami_1,d17_ami_1,d15_ami_1,t14_ami_3,d2_tarski]),
    [file(ami_6,t48_ami_6),interesting(0.00)]).

fof(d4_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k4_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & ~ r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d4_xboole_0),
    [interesting(0.00)]).

fof(t15_ami_3,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_ami_3(B)
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => ! [D] : 
                  ( m1_subset_1(D,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
                 => ( ( ~ r1_xreal_0(k2_ami_3(D,A),0)
                     => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(C,A),D),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = C )
                    & ( r1_xreal_0(k2_ami_3(D,A),0)
                     => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(C,A),D),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,D)) )
                    & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(C,A),D),B) = k2_ami_3(D,B) ) ) ) ) ) ),
    file(ami_3,t15_ami_3),
    [interesting(0.00)]).

fof(t50_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => ! [C] : 
              ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => k1_amistd_1(k1_tarski(k4_numbers),k1_ami_3,C,k10_ami_3(B,A)) = k2_struct_0(k1_ami_3,B,k11_ami_3(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_ami_1,d17_ami_1,d15_ami_1,t15_ami_3,d2_tarski,t15_ami_3,d2_tarski,d3_tarski,d10_xboole_0,d3_tarski,d11_ami_1,d14_ami_1,t1_ami_6,t20_ami_5,t5_cqc_lang,d1_tarski,d15_ami_1,t12_funct_4,d15_ami_1,t6_ami_6,d1_tarski,t12_funct_4,t6_ami_6,d1_tarski,t14_funct_4,t6_cqc_lang,d18_ami_1,d17_ami_1,d15_ami_1,t15_ami_3,t5_cqc_lang,d1_tarski,d15_ami_1,t12_funct_4,d15_ami_1,t6_ami_6,d1_tarski,t12_funct_4,t6_ami_6,d1_tarski,t14_funct_4,t6_cqc_lang,d18_ami_1,d17_ami_1,d15_ami_1,t15_ami_3,d2_tarski]),
    [file(ami_6,t50_ami_6),interesting(0.00)]).

fof(t69_ami_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
    <=> ~ ( A != k4_tarski(0,k1_xboole_0)
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k3_ami_3(B,C) ) )
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k4_ami_3(B,C) ) )
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k5_ami_3(B,C) ) )
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k6_ami_3(B,C) ) )
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k7_ami_3(B,C) ) )
          & ! [B] : 
              ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => A != k8_ami_3(B) )
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
                 => A != k9_ami_3(C,B) ) )
          & ! [B] : 
              ( m1_ami_3(B)
             => ! [C] : 
                  ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
                 => A != k10_ami_3(C,B) ) ) ) ) ),
    file(ami_3,t69_ami_3),
    [interesting(0.00)]).

fof(t54_ami_3,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k11_ami_3(k16_ami_3(A)) = k16_ami_3(k2_xcmplx_0(A,1)) ) ),
    file(ami_3,t54_ami_3),
    [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(t18_amistd_1,theorem,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,u2_ami_1(A,B))
                & m2_relset_1(C,k5_numbers,u2_ami_1(A,B)) )
             => ( v3_funct_2(C,k5_numbers,u2_ami_1(A,B))
               => ( ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( r1_xreal_0(D,E)
                          <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D),k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E)) ) ) )
                <=> ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(A,B),C,k1_nat_1(D,1)),k3_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D)))
                        & ! [E] : 
                            ( m2_subset_1(E,k1_numbers,k5_numbers)
                           => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E),k3_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D)))
                             => r1_xreal_0(D,E) ) ) ) ) ) ) ) ) ) ),
    file(amistd_1,t18_amistd_1),
    [interesting(0.00)]).

fof(d21_ordinal2,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
    <=> r2_hidden(A,k5_ordinal2) ) ),
    file(ordinal2,d21_ordinal2),
    [interesting(0.00)]).

fof(d12_amistd_1,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & v4_amistd_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( v4_ordinal2(C)
             => ! [D] : 
                  ( m1_struct_0(D,B,u2_ami_1(A,B))
                 => ( D = k5_amistd_1(A,B,C)
                  <=> ? [E] : 
                        ( v1_funct_1(E)
                        & v1_funct_2(E,k5_numbers,u2_ami_1(A,B))
                        & m2_relset_1(E,k5_numbers,u2_ami_1(A,B))
                        & v3_funct_2(E,k5_numbers,u2_ami_1(A,B))
                        & ! [F] : 
                            ( m2_subset_1(F,k1_numbers,k5_numbers)
                           => ! [G] : 
                                ( m2_subset_1(G,k1_numbers,k5_numbers)
                               => ( r1_xreal_0(F,G)
                                <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),E,F),k8_funct_2(k5_numbers,u2_ami_1(A,B),E,G)) ) ) )
                        & D = k1_funct_1(E,C) ) ) ) ) ) ) ),
    file(amistd_1,d12_amistd_1),
    [interesting(0.00)]).

fof(d13_amistd_1,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & v4_amistd_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m1_struct_0(C,B,u2_ami_1(A,B))
             => ! [D] : 
                  ( v4_ordinal2(D)
                 => ( D = k6_amistd_1(A,B,C)
                  <=> k5_amistd_1(A,B,D) = C ) ) ) ) ) ),
    file(amistd_1,d13_amistd_1),
    [interesting(0.00)]).

fof(d14_amistd_2,definition,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & ~ v2_ami_1(B,A)
            & v5_ami_1(B,A)
            & v8_ami_1(B,A)
            & v4_amistd_1(B,A)
            & v8_amistd_2(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B))
             => ! [D] : 
                  ( v4_ordinal2(D)
                 => ! [E] : 
                      ( m2_subset_1(E,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B))
                     => ( E = k8_amistd_2(A,B,C,D)
                      <=> ( k1_ami_5(A,B,E) = k1_ami_5(A,B,C)
                          & k4_finseq_1(k4_amistd_2(A,B,E)) = k4_finseq_1(k4_amistd_2(A,B,C))
                          & ! [F] : 
                              ( r2_hidden(F,k4_finseq_1(k4_amistd_2(A,B,C)))
                             => ( ~ ( k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),F) = u2_ami_1(A,B)
                                    & ! [G] : 
                                        ( m1_struct_0(G,B,u2_ami_1(A,B))
                                       => ~ ( G = k1_funct_1(k4_amistd_2(A,B,C),F)
                                            & k1_funct_1(k4_amistd_2(A,B,E),F) = k5_amistd_1(A,B,k2_xcmplx_0(D,k7_amistd_1(A,B,G))) ) ) )
                                & ( k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),F) != u2_ami_1(A,B)
                                 => k1_funct_1(k4_amistd_2(A,B,E),F) = k1_funct_1(k4_amistd_2(A,B,C),F) ) ) ) ) ) ) ) ) ) ) ),
    file(amistd_2,d14_amistd_2),
    [interesting(0.00)]).

fof(t43_ami_5,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(A)) = 6 ) ),
    file(ami_5,t43_ami_5),
    [interesting(0.00)]).

fof(d8_ami_3,definition,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k8_ami_3(A) = k4_tarski(6,k12_finseq_1(u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A)) ) ),
    file(ami_3,d8_ami_3),
    [interesting(0.00)]).

fof(t13_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k4_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(A)) = k12_finseq_1(u2_ami_1(k1_tarski(k4_numbers),k1_ami_3),A) ) ),
    inference(mizar_proof,[status(thm)],[d8_ami_3,d2_mcart_1]),
    [file(ami_6,t13_ami_6),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(t52_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 6
          & ! [B] : 
              ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => A != k8_ami_3(B) ) ) ) ),
    file(ami_5,t52_ami_5),
    [interesting(0.00)]).

fof(t22_ami_6,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u3_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ( A = 6
       => k1_relat_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,A))) = k1_tarski(1) ) ) ),
    inference(mizar_proof,[status(thm)],[t13_ami_6,t43_ami_5,d1_amistd_2,t4_finseq_1,d8_finseq_1,d3_tarski,d10_xboole_0,d3_tarski,t52_ami_5,t13_ami_6,t4_finseq_1,d8_finseq_1,d1_amistd_2]),
    [file(ami_6,t22_ami_6),interesting(0.00)]).

fof(t8_amistd_2,theorem,(
    ! [A] : 
      ( v1_fraenkel(A)
     => ! [B] : 
          ( r2_hidden(B,k1_relat_1(k1_amistd_2(A)))
         => k1_funct_1(k1_amistd_2(A),B) = k5_card_3(B,A) ) ) ),
    file(amistd_2,t8_amistd_2),
    [interesting(0.00)]).

fof(t35_ami_6,theorem,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => k1_funct_1(k1_amistd_2(k5_amistd_2(k1_tarski(k4_numbers),k1_ami_3,k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k8_ami_3(A)))),1) = u2_ami_1(k1_tarski(k4_numbers),k1_ami_3) ) ),
    inference(mizar_proof,[status(thm)],[t43_ami_5,t22_ami_6,d1_tarski,t43_ami_5,t8_amistd_2,d6_card_3,t52_ami_5,t13_ami_6,d8_finseq_1,d3_tarski,d10_xboole_0,d3_tarski,t13_ami_6,t43_ami_5,d8_finseq_1,d6_card_3,t8_amistd_2]),
    [file(ami_6,t35_ami_6),interesting(0.00)]).

fof(t9_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( k1_relat_1(A) = k1_relat_1(B)
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) )
           => A = B ) ) ) ),
    file(funct_1,t9_funct_1),
    [interesting(0.00)]).

fof(t16_amistd_2,theorem,(
    ! [A,B] : 
      ( l1_ami_1(B,A)
     => ! [C] : 
          ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B))
         => ! [D] : 
              ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B))
             => ( ( k1_ami_5(A,B,C) = k1_ami_5(A,B,D)
                  & k4_amistd_2(A,B,C) = k4_amistd_2(A,B,D) )
               => C = D ) ) ) ) ),
    file(amistd_2,t16_amistd_2),
    [interesting(0.00)]).

fof(t44_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k9_ami_3(B,A)) = 7 ) ) ),
    file(ami_5,t44_ami_5),
    [interesting(0.00)]).

fof(d9_ami_3,definition,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( m1_ami_3(B)
         => k9_ami_3(A,B) = k4_tarski(7,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d9_ami_3),
    [interesting(0.00)]).

fof(t53_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 7
          & ! [B] : 
              ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k9_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t53_ami_5),
    [interesting(0.00)]).

fof(t12_ami_2,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k5_numbers,k3_ami_2)
     => ! [B] : 
          ( m2_subset_1(B,k5_numbers,k2_ami_2)
         => A != B ) ) ),
    file(ami_2,t12_ami_2),
    [interesting(0.00)]).

fof(t45_ami_5,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
         => k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(B,A)) = 8 ) ) ),
    file(ami_5,t45_ami_5),
    [interesting(0.00)]).

fof(d10_ami_3,definition,(
    ! [A] : 
      ( m1_struct_0(A,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ! [B] : 
          ( m1_ami_3(B)
         => k10_ami_3(A,B) = k4_tarski(8,k10_finseq_1(A,B)) ) ) ),
    file(ami_3,d10_ami_3),
    [interesting(0.00)]).

fof(t54_ami_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k2_zfmisc_1(u3_ami_1(k1_tarski(k4_numbers),k1_ami_3),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),u1_struct_0(k1_ami_3)))),u4_ami_1(k1_tarski(k4_numbers),k1_ami_3))
     => ~ ( k1_ami_5(k1_tarski(k4_numbers),k1_ami_3,A) = 8
          & ! [B] : 
              ( m1_struct_0(B,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
             => ! [C] : 
                  ( m1_ami_3(C)
                 => A != k10_ami_3(B,C) ) ) ) ) ),
    file(ami_5,t54_ami_5),
    [interesting(0.00)]).

fof(t36_ami_3,theorem,(
    ! [A] : 
      ( v1_setfam_1(A)
     => ! [B] : 
          ( ( ~ v2_ami_1(B,A)
            & l1_ami_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B)))
             => k1_relat_1(C) = u1_struct_0(B) ) ) ) ),
    file(ami_3,t36_ami_3),
    [interesting(0.00)]).

fof(d3_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k3_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d3_xboole_0),
    [interesting(0.00)]).

fof(t71_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,k3_xboole_0(k1_relat_1(C),A))
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t71_funct_1),
    [interesting(0.00)]).

fof(d2_funct_7,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : 
              ( r1_funct_7(A,B,C)
            <=> k7_relat_1(A,k4_xboole_0(k1_relat_1(A),C)) = k7_relat_1(B,k4_xboole_0(k1_relat_1(B),C)) ) ) ) ),
    file(funct_7,d2_funct_7),
    [interesting(0.00)]).

fof(t5_ami_6,theorem,(
    ! [A] : 
      ( m1_ami_3(A)
     => ! [B] : 
          ( m1_subset_1(B,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
         => ! [C] : 
              ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3)))
             => ( r1_funct_7(B,C,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3))
               => k2_ami_3(B,A) = k2_ami_3(C,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t36_ami_3,t36_ami_3,t1_ami_6,d4_xboole_0,d3_xboole_0,d4_xboole_0,d3_xboole_0,t71_funct_1,d2_funct_7,t71_funct_1]),
    [file(ami_6,t5_ami_6),interesting(0.00)]).