fof(t25_armstrng,theorem,(
    ! [A] : 
      ( l1_armstrng(A)
     => v6_armstrng(k5_armstrng(A),u1_armstrng(A)) ) ),
    inference(mizar_proof,[status(thm)],[d16_armstrng,d8_armstrng,t103_relat_1,t103_relat_1,t12_armstrng,d8_armstrng,d8_armstrng,d8_armstrng,t20_armstrng,t23_armstrng,d15_armstrng,t20_armstrng,t23_armstrng,d14_armstrng,t12_armstrng,d8_armstrng,t7_xboole_1,t103_relat_1,t103_relat_1,d8_armstrng,t103_relat_1,t103_relat_1,d8_armstrng,t107_relat_1,t107_relat_1]),
    [file(armstrng,t25_armstrng),interesting(1.00)]).

fof(t61_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => k14_armstrng(A,B) = k14_armstrng(A,k12_armstrng(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_armstrng,d25_armstrng,t57_armstrng,t57_armstrng,t57_armstrng,t40_armstrng,t33_zfmisc_1,t2_tarski]),
    [file(armstrng,t61_armstrng),interesting(0.92)]).

fof(t62_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ( r2_hidden(C,k13_armstrng(A,k12_armstrng(A,B)))
              <=> r6_armstrng(A,C,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t40_armstrng,d4_subset_1,d18_armstrng,t29_armstrng,t33_zfmisc_1,d10_xboole_0,d33_armstrng,d8_xboole_0,t1_xboole_1,d3_tarski,d12_armstrng,t18_finset_1,d12_armstrng,d14_armstrng,t7_xboole_1,d4_subset_1,t61_armstrng,t57_armstrng,d12_armstrng,d14_armstrng,t12_xboole_1,t20_armstrng,t7_xboole_1,t10_xboole_1,t10_xboole_1,t7_xboole_1,d8_xboole_0,t15_armstrng,t29_armstrng,d3_tarski,d12_armstrng,t18_finset_1,d12_armstrng,d14_armstrng,t7_xboole_1,d4_subset_1,d33_armstrng,t61_armstrng,t57_armstrng,d12_armstrng,d14_armstrng,t12_xboole_1,t20_armstrng,t7_xboole_1,t10_xboole_1,t10_xboole_1,t7_xboole_1,t15_armstrng,d10_xboole_0,d8_xboole_0,d10_xboole_0,d33_armstrng,t61_armstrng,d10_xboole_0,t29_armstrng,d18_armstrng]),
    [file(armstrng,t62_armstrng),interesting(0.91)]).

fof(t60_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
             => ( k14_armstrng(A,B) = k14_armstrng(A,C)
               => k12_armstrng(A,B) = k12_armstrng(A,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_armstrng,t59_armstrng,t59_armstrng,t10_armstrng,t59_armstrng,t59_armstrng,t2_tarski]),
    [file(armstrng,t60_armstrng),interesting(0.90)]).

fof(t40_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => k12_armstrng(A,B) = k10_armstrng(A,k11_armstrng(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_armstrng,t39_armstrng,t39_armstrng,d25_armstrng]),
    [file(armstrng,t40_armstrng),interesting(0.90)]).

fof(t36_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => r1_tarski(B,k9_armstrng(A,k10_armstrng(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_armstrng,t30_armstrng,d3_tarski,d19_armstrng,t15_armstrng,t33_zfmisc_1,d10_xboole_0,d18_armstrng]),
    [file(armstrng,t36_armstrng),interesting(0.87)]).

fof(t35_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => v6_armstrng(k10_armstrng(A,B),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_zfmisc_1,t2_tarski,t21_armstrng,d15_armstrng,t33_zfmisc_1,d12_armstrng,d15_armstrng,t20_armstrng,d13_armstrng,t15_armstrng,t1_xboole_1,t1_xboole_1,d14_armstrng,t11_xboole_1,t8_xboole_1]),
    [file(armstrng,t35_armstrng),interesting(0.84)]).

fof(t21_armstrng,theorem,(
    ! [A] : 
      ( v3_armstrng(k4_armstrng(A),A)
      & v8_relat_2(k4_armstrng(A))
      & v4_armstrng(k4_armstrng(A),A)
      & v5_armstrng(k4_armstrng(A),A) ) ),
    inference(mizar_proof,[status(thm)],[d1_eqrel_1,t97_orders_1,d12_armstrng,d8_relat_2,d16_relat_2,d2_zfmisc_1,d13_armstrng,d14_armstrng]),
    [file(armstrng,t21_armstrng),interesting(0.79)]).

fof(t13_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k4_armstrng(A))
     => ! [C] : 
          ( m1_subset_1(C,k4_armstrng(A))
         => ( ( r3_armstrng(A,C,B)
              & r3_armstrng(A,B,C) )
           => B = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_armstrng,d10_xboole_0,t24_mcart_1]),
    [file(armstrng,t13_armstrng),interesting(0.78)]).

fof(t44_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => r5_armstrng(A,B,k9_armstrng(A,k10_armstrng(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_armstrng,t34_armstrng,t36_armstrng,d26_armstrng,t33_armstrng,d18_armstrng,t33_zfmisc_1,d3_tarski,t4_mssubfam,d3_tarski,t2_mssubfam,t15_armstrng,t29_armstrng,t1_xboole_1,t24_finset_1,t13_finset_1,d4_armstrng,t1_armstrng,t2_tarski]),
    [file(armstrng,t44_armstrng),interesting(0.78)]).

fof(t22_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => v1_finset_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_finset_1,t19_finset_1,t13_finset_1]),
    [file(armstrng,t22_armstrng),interesting(0.74)]).

fof(t19_armstrng,theorem,(
    ! [A] : k3_relat_1(k7_armstrng(A)) = k2_zfmisc_1(k1_zfmisc_1(A),k1_zfmisc_1(A)) ),
    inference(mizar_proof,[status(thm)],[d6_relat_1,t17_armstrng,t18_armstrng]),
    [file(armstrng,t19_armstrng),interesting(0.74)]).

fof(t50_armstrng,theorem,(
    ! [A] : 
      ( l1_armstrng(A)
     => ( ~ v1_xboole_0(k13_armstrng(u1_armstrng(A),k5_armstrng(A)))
        & v11_armstrng(k13_armstrng(u1_armstrng(A),k5_armstrng(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_armstrng,t34_armstrng,d4_armstrng,t33_armstrng,d18_armstrng,d28_armstrng,t30_armstrng,d4_subset_1,t15_armstrng,d20_armstrng]),
    [file(armstrng,t50_armstrng),interesting(0.73)]).

fof(t14_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k4_armstrng(A))
     => ! [C] : 
          ( m1_subset_1(C,k4_armstrng(A))
         => ! [D] : 
              ( m1_subset_1(D,k4_armstrng(A))
             => ( ( r3_armstrng(A,C,B)
                  & r3_armstrng(A,D,C) )
               => r3_armstrng(A,D,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_armstrng,t1_xboole_1,d10_armstrng]),
    [file(armstrng,t14_armstrng),interesting(0.72)]).

fof(t34_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( ( v6_armstrng(B,A)
            & m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
         => ( v1_armstrng(k9_armstrng(A,B),A)
            & v2_finsub_1(k9_armstrng(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_subset_1,t30_armstrng,d19_armstrng,d18_armstrng,t15_armstrng,d10_xboole_0,d4_armstrng,d2_finsub_1,t33_armstrng,d18_armstrng,t33_armstrng,d18_armstrng,d19_armstrng,d18_armstrng,t15_armstrng,t17_xboole_1,t1_xboole_1,t30_armstrng,d21_armstrng,t17_xboole_1,t1_xboole_1,d21_armstrng,t19_xboole_1,d10_xboole_0]),
    [file(armstrng,t34_armstrng),interesting(0.71)]).

fof(t1_armstrng,theorem,(
    ! [A] : 
      ( v2_finsub_1(A)
     => ! [B,C] : 
          ( ( v1_finset_1(C)
            & m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(B))) )
         => ( ( r2_hidden(B,A)
              & r1_tarski(C,A) )
           => r2_hidden(k8_setfam_1(B,C),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_setfam_1,t1_xboole_1,t37_zfmisc_1,t8_mssubfam,t9_mssubfam,d2_finsub_1,s2_finset_1]),
    [file(armstrng,t1_armstrng),interesting(0.70)]).

fof(t26_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ( v6_armstrng(a_2_0_armstrng(A,B),A)
        & m2_relset_1(a_2_0_armstrng(A,B),k1_zfmisc_1(A),k1_zfmisc_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_relset_1,t33_zfmisc_1,t1_xboole_1,t20_armstrng,d16_armstrng,t23_armstrng,d15_armstrng,t20_armstrng,t23_armstrng,d14_armstrng,t33_zfmisc_1,t10_xboole_1,t13_xboole_1]),
    [file(armstrng,t26_armstrng),interesting(0.68)]).

fof(t17_armstrng,theorem,(
    ! [A] : k4_relset_1(k4_armstrng(A),k4_armstrng(A),k7_armstrng(A)) = k2_zfmisc_1(k1_zfmisc_1(A),k1_zfmisc_1(A)) ),
    inference(mizar_proof,[status(thm)],[d4_relat_1,t2_tarski]),
    [file(armstrng,t17_armstrng),interesting(0.67)]).

fof(t18_armstrng,theorem,(
    ! [A] : k5_relset_1(k4_armstrng(A),k4_armstrng(A),k7_armstrng(A)) = k2_zfmisc_1(k1_zfmisc_1(A),k1_zfmisc_1(A)) ),
    inference(mizar_proof,[status(thm)],[d5_relat_1,t2_tarski]),
    [file(armstrng,t18_armstrng),interesting(0.67)]).

fof(s2_armstrng,theorem,
    ( ( ! [A] : 
          ( r1_armstrng(A,f1_s2_armstrng)
         => p1_s2_armstrng(A) )
      & ! [A,B] : 
          ( ( r2_hidden(A,f1_s2_armstrng)
            & r2_hidden(B,f1_s2_armstrng)
            & p1_s2_armstrng(A)
            & p1_s2_armstrng(B) )
         => p1_s2_armstrng(k3_xboole_0(A,B)) ) )
   => ! [A] : 
        ( r2_hidden(A,f1_s2_armstrng)
       => p1_s2_armstrng(A) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t13_finset_1,s5_nat_1,d2_armstrng,t17_xboole_1,d3_tarski,t13_finset_1,d3_tarski,t13_finset_1,d3_tarski,t13_finset_1,d10_xboole_0,d10_xboole_0,d3_tarski,t1_xboole_1,d3_tarski,t1_xboole_1,d8_xboole_0,t24_trees_1]),
    [file(armstrng,s2_armstrng),interesting(0.66)]).

fof(t15_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ! [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(A))
             => ! [E] : 
                  ( m1_subset_1(E,k1_zfmisc_1(A))
                 => ( r3_armstrng(A,k6_armstrng(A,B,C),k6_armstrng(A,D,E))
                  <=> ( r1_tarski(B,D)
                      & r1_tarski(E,C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_mcart_1,d2_mcart_1,d10_armstrng]),
    [file(armstrng,t15_armstrng),interesting(0.65)]).

fof(t30_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( ( v6_armstrng(B,A)
            & m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
         => ( v8_armstrng(k8_armstrng(A,B),A)
            & v9_armstrng(k8_armstrng(A,B),A)
            & v10_armstrng(k8_armstrng(A,B),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d19_armstrng,t19_armstrng,s1_xboole_0,d16_armstrng,d3_tarski,t13_finset_1,t1_xboole_1,t2_armstrng,d24_waybel_4,d2_zfmisc_1,d24_waybel_4,t33_zfmisc_1,t14_armstrng,d24_waybel_4,d1_armstrng,d20_armstrng,d1_armstrng,t33_zfmisc_1,d24_waybel_4,d21_armstrng,t15_armstrng,d18_armstrng,t29_armstrng,d13_armstrng,d18_armstrng,t29_armstrng,t20_armstrng,d14_armstrng,t7_xboole_1,t15_armstrng,t29_armstrng,t11_xboole_1]),
    [file(armstrng,t30_armstrng),interesting(0.65)]).

fof(t3_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ? [C] : 
              ( ~ v1_xboole_0(C)
              & m1_subset_1(C,k1_zfmisc_1(A))
              & B = k1_setfam_1(C)
              & ! [D] : 
                  ( r2_hidden(D,C)
                 => r1_armstrng(D,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_armstrng,t37_zfmisc_1,t11_setfam_1,d1_tarski,t10_setfam_1,d2_xboole_0,s2_armstrng]),
    [file(armstrng,t3_armstrng),interesting(0.65)]).

fof(t9_armstrng,theorem,(
    ! [A,B] : 
      ( r2_hidden(B,k4_armstrng(A))
    <=> ? [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
          & ? [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(A))
              & B = k4_tarski(C,D) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t102_zfmisc_1,t106_zfmisc_1,t106_zfmisc_1]),
    [file(armstrng,t9_armstrng),interesting(0.62)]).

fof(t45_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( ( v6_armstrng(B,A)
            & m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
         => ? [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
              & r5_armstrng(A,C,k9_armstrng(A,B))
              & B = k10_armstrng(A,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t34_armstrng,d26_armstrng,t37_zfmisc_1,t37_zfmisc_1,d10_setfam_1,t11_setfam_1,t24_finset_1,t13_finset_1,d4_armstrng,t1_armstrng,t2_tarski,t37_armstrng]),
    [file(armstrng,t45_armstrng),interesting(0.62)]).

fof(l76_armstrng,theorem,(
    ! [A,B,C] : 
      ( B = a_2_5_armstrng(A,C)
     => ! [D] : 
          ( m1_subset_1(D,k1_zfmisc_1(A))
         => ! [E] : 
              ( m1_subset_1(E,k1_zfmisc_1(A))
             => ( r2_hidden(k6_armstrng(A,D,E),B)
              <=> ! [F] : 
                    ( ( r2_hidden(F,C)
                      & r1_tarski(D,F) )
                   => r1_tarski(E,F) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_zfmisc_1]),
    [file(armstrng,l76_armstrng),interesting(0.62)]).

fof(t10_armstrng,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ~ ( r2_hidden(B,C)
          & ! [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(A))
             => ! [E] : 
                  ( m1_subset_1(E,k1_zfmisc_1(A))
                 => B != k4_tarski(D,E) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t102_zfmisc_1,t106_zfmisc_1]),
    [file(armstrng,t10_armstrng),interesting(0.61)]).

fof(t49_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ( B = a_2_2_armstrng(A,C)
               => k13_armstrng(A,B) = k1_tarski(C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_armstrng,d1_tarski,t33_zfmisc_1,d1_tarski,t33_zfmisc_1,d2_xboole_0,d1_tarski,d1_tarski,d2_xboole_0,t2_tarski]),
    [file(armstrng,t49_armstrng),interesting(0.61)]).

fof(t32_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ( B = a_2_2_armstrng(A,C)
               => k2_xboole_0(k1_tarski(k4_tarski(C,A)),a_2_3_armstrng(A,C)) = k8_armstrng(A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_subset_1,d1_tarski,t7_xboole_1,t7_xboole_1,d1_tarski,t33_zfmisc_1,d2_xboole_0,d3_tarski,d1_tarski,d2_zfmisc_1,d2_xboole_0,d1_relset_1,d19_armstrng,t15_armstrng,d4_subset_1,d20_armstrng,t15_armstrng,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,d10_xboole_0,d10_xboole_0,d21_armstrng,t33_zfmisc_1,t33_zfmisc_1,d3_tarski,d1_relset_1,t31_armstrng,t7_xboole_1,d1_tarski,t7_xboole_1,t15_armstrng,t15_armstrng,d1_tarski,t33_zfmisc_1,t15_armstrng,t33_zfmisc_1,t15_armstrng,t1_xboole_1,d2_xboole_0,t2_tarski]),
    [file(armstrng,t32_armstrng),interesting(0.57)]).

fof(t12_armstrng,theorem,(
    ! [A] : 
      ( l1_armstrng(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_armstrng(A)))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(u1_armstrng(A)))
             => ( r2_hidden(k4_tarski(B,C),k5_armstrng(A))
              <=> r2_armstrng(A,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_zfmisc_1]),
    [file(armstrng,t12_armstrng),interesting(0.57)]).

fof(t41_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( C = k2_xboole_0(k1_tarski(A),a_2_7_armstrng(A,B))
           => ( v1_armstrng(C,A)
              & v2_finsub_1(C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d2_xboole_0,d4_armstrng,d2_finsub_1,d1_tarski,d1_tarski,d2_xboole_0,d1_tarski,t28_xboole_1,d2_xboole_0,d1_tarski,t28_xboole_1,d2_xboole_0,t18_xboole_1,d2_xboole_0,d2_xboole_0]),
    [file(armstrng,t41_armstrng),interesting(0.56)]).

fof(t46_armstrng,theorem,(
    ! [A,B] : 
      ( ( ~ v1_xboole_0(B)
        & v1_finset_1(B)
        & m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) )
     => ( ( v1_armstrng(B,A)
          & v2_finsub_1(B) )
       => r5_armstrng(A,k2_armstrng(B),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_armstrng,d26_armstrng,t3_armstrng,t1_xboole_1,d10_setfam_1,d3_tarski,d3_armstrng,t1_xboole_1,t13_finset_1,t1_armstrng,t2_tarski]),
    [file(armstrng,t46_armstrng),interesting(0.56)]).

fof(t38_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ( v1_armstrng(k11_armstrng(A,B),A)
            & v2_finsub_1(k11_armstrng(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_subset_1,d4_armstrng,d2_finsub_1,t18_xboole_1,t19_xboole_1]),
    [file(armstrng,t38_armstrng),interesting(0.55)]).

fof(l1_armstrng,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_2(C,B,k4_finseq_2(A,B))
             => k4_finseq_1(C) = k2_finseq_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t109_finseq_2,d3_finseq_1]),
    [file(armstrng,l1_armstrng),interesting(0.53)]).

fof(t43_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ( B = a_2_2_armstrng(A,C)
               => k2_xboole_0(k1_tarski(A),a_2_10_armstrng(A,C)) = k9_armstrng(A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_armstrng,d4_subset_1,d1_tarski,d1_tarski,d2_xboole_0,d18_armstrng,d2_xboole_0,d18_armstrng,d2_xboole_0,t33_armstrng,d18_armstrng,d1_tarski,t33_zfmisc_1,d1_tarski,d2_xboole_0,t33_zfmisc_1,d2_xboole_0,d2_xboole_0,t2_tarski]),
    [file(armstrng,t43_armstrng),interesting(0.47)]).

fof(t5_armstrng,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1))
         => k3_armstrng(A,k1_binari_3(A,0),B) = k1_binari_3(A,0) ) ) ),
    inference(mizar_proof,[status(thm)],[l1_armstrng,l1_armstrng,l1_armstrng,t26_binari_3,d4_euclid,t70_finseq_2,d4_finseq_4,d13_margrel1,d5_armstrng,t49_margrel1,t70_finseq_2,d13_margrel1,t9_funct_1]),
    [file(armstrng,t5_armstrng),interesting(0.47)]).

fof(t51_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ~ ( ~ v1_xboole_0(B)
              & v11_armstrng(B)
              & ! [C] : 
                  ( ( v6_armstrng(C,A)
                    & m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
                 => B != k13_armstrng(A,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t35_armstrng,d4_subset_1,t28_armstrng,t15_armstrng,t15_armstrng,d10_xboole_0,t1_xboole_1,d28_armstrng,d10_xboole_0,l76_armstrng,d10_xboole_0,d10_xboole_0,l76_armstrng,d10_xboole_0,d18_armstrng,d18_armstrng,t29_armstrng,t15_armstrng,t29_armstrng,d1_xboole_0,t2_tarski]),
    [file(armstrng,t51_armstrng),interesting(0.47)]).

fof(t52_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ! [C] : 
              ( ( v11_armstrng(B)
                & C = a_2_13_armstrng(A,B) )
             => ( v1_xboole_0(B)
                | B = k13_armstrng(A,k10_armstrng(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_subset_1,t28_armstrng,t15_armstrng,t15_armstrng,d10_xboole_0,t1_xboole_1,d28_armstrng,d10_xboole_0,l76_armstrng,d10_xboole_0,d10_xboole_0,l76_armstrng,d10_xboole_0,d18_armstrng,d18_armstrng,t29_armstrng,t15_armstrng,t29_armstrng,d1_xboole_0,t2_tarski]),
    [file(armstrng,t52_armstrng),interesting(0.47)]).

fof(s1_armstrng,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(f1_s1_armstrng))
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(f1_s1_armstrng))
         => ( ( ! [C] : 
                  ( r2_hidden(C,A)
                <=> p1_s1_armstrng(C) )
              & ! [C] : 
                  ( r2_hidden(C,B)
                <=> p1_s1_armstrng(C) ) )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_tarski]),
    [file(armstrng,s1_armstrng),interesting(0.46)]).

fof(t42_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ( B = a_2_8_armstrng(A,C)
               => k2_xboole_0(k1_tarski(A),a_2_9_armstrng(A,C)) = k9_armstrng(A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t80_zfmisc_1,d2_xboole_0,t41_armstrng,t41_armstrng,d1_tarski,t1_xboole_1,d2_xboole_0,t1_xboole_1,d2_xboole_0,t2_tarski,t37_armstrng]),
    [file(armstrng,t42_armstrng),interesting(0.41)]).

fof(t53_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ~ ( ~ v1_xboole_0(B)
              & v11_armstrng(B)
              & ! [C] : 
                  ( l1_armstrng(C)
                 => ~ ( u1_armstrng(C) = A
                      & B = k13_armstrng(u1_armstrng(C),k5_armstrng(C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d2_xboole_0,d3_tarski,t19_funcop_1,d1_funct_4,t19_funcop_1,t12_xboole_1,d3_pboole,t13_funcop_1,t14_funct_4,t13_funcop_1,t12_funct_4,t13_funcop_1,d5_card_3,d4_subset_1,d2_xboole_0,t19_funcop_1,t19_funcop_1,d1_xboole_0,d3_xboole_0,t72_funct_1,t14_funct_4,t13_funcop_1,t72_funct_1,t14_funct_4,t13_funcop_1,t12_funct_4,t13_funcop_1,d1_xboole_0,d3_xboole_0,t16_funcop_1,t72_funct_1,t64_relat_1,t22_funct_4,t13_funcop_1,t72_funct_1,t14_funct_4,t13_funcop_1,d1_xboole_0,d3_xboole_0,t16_funcop_1,t72_funct_1,t64_relat_1,t22_funct_4,t13_funcop_1,t72_funct_1,t14_funct_4,t13_funcop_1,d1_tarski,d8_armstrng,t28_armstrng,t15_armstrng,d10_xboole_0,t33_zfmisc_1,d1_tarski,d2_xboole_0,d7_xboole_0,t44_subset_1,t1_xboole_1,d28_armstrng,d10_xboole_0,d2_xboole_0,t19_funcop_1,t22_funct_4,t90_relat_1,t19_funcop_1,d1_funct_4,t19_funcop_1,t19_funcop_1,t12_xboole_1,t90_relat_1,d3_xboole_0,t26_subset_1,d7_xboole_0,d3_xboole_0,t72_funct_1,t12_funct_4,t68_funct_1,t2_xboole_1,t39_subset_1,d10_xboole_0,d1_xboole_0,t72_funct_1,t13_funcop_1,t72_funct_1,t14_funct_4,t13_funcop_1,d8_armstrng,d10_xboole_0,d18_armstrng,t15_armstrng,t29_armstrng,d1_xboole_0,d3_tarski,d3_tarski,d3_tarski,d3_xboole_0,d1_tarski,d2_xboole_0,d2_xboole_0,t22_funct_4,t19_funcop_1,t90_relat_1,t19_funcop_1,d1_funct_4,t19_funcop_1,t19_funcop_1,t12_xboole_1,t90_relat_1,d3_xboole_0,d3_xboole_0,t72_funct_1,t12_funct_4,t68_funct_1,t33_zfmisc_1,t72_funct_1,t13_funcop_1,t72_funct_1,t14_funct_4,t13_funcop_1,d8_armstrng,t2_tarski]),
    [file(armstrng,t53_armstrng),interesting(0.41)]).

fof(t37_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( ( v1_armstrng(B,A)
              & v2_finsub_1(B) )
           => ( B = k9_armstrng(A,k10_armstrng(A,B))
              & ! [C] : 
                  ( ( v6_armstrng(C,A)
                    & m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
                 => ( B = k9_armstrng(A,C)
                   => C = k10_armstrng(A,B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_armstrng,d4_armstrng,d4_armstrng,t36_armstrng,t33_armstrng,d18_armstrng,t33_zfmisc_1,t24_finset_1,d3_tarski,t13_finset_1,d3_tarski,d3_tarski,d1_setfam_1,d10_setfam_1,t4_setfam_1,d10_setfam_1,t15_armstrng,t29_armstrng,t1_armstrng,t2_tarski,t30_armstrng,t9_armstrng,t33_armstrng,d18_armstrng,t28_armstrng,t15_armstrng,t1_xboole_1,d21_armstrng,t15_armstrng,t1_xboole_1,d19_armstrng,t15_armstrng,d18_armstrng,t15_armstrng,d13_armstrng,t2_tarski]),
    [file(armstrng,t37_armstrng),interesting(0.38)]).

fof(t2_armstrng,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & ~ v1_xboole_0(A)
        & v4_relat_2(A)
        & v8_relat_2(A) )
     => ! [B] : 
          ( ( v1_finset_1(B)
            & m1_subset_1(B,k1_zfmisc_1(k3_relat_1(A))) )
         => ~ ( B != k1_xboole_0
              & ! [C] : 
                  ( m1_subset_1(C,B)
                 => ~ r2_waybel_4(B,C,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_polynom1,t3_xboole_1,d12_relat_2,d3_yellow_0,d9_orders_2,d4_relat_2,d16_relat_2,d2_yellow_0,d9_orders_2,d8_relat_2,d9_orders_2,d1_struct_0,t7_bagorder,d24_waybel_4,d24_waybel_4]),
    [file(armstrng,t2_armstrng),interesting(0.37)]).

fof(t31_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
             => ( ( v8_armstrng(B,A)
                  & v9_armstrng(B,A)
                  & v10_armstrng(B,A)
                  & C = a_2_1_armstrng(A,B) )
               => ( B = k8_armstrng(A,C)
                  & v6_armstrng(C,A)
                  & ! [D] : 
                      ( ( v6_armstrng(D,A)
                        & m2_relset_1(D,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
                     => ( B = k8_armstrng(A,D)
                       => D = C ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_armstrng,d24_waybel_4,t33_zfmisc_1,t14_armstrng,d20_armstrng,t13_armstrng,d1_armstrng,d1_armstrng,d24_waybel_4,t2_tarski,d12_armstrng,d19_armstrng,d15_armstrng,t15_armstrng,t1_xboole_1,d21_armstrng,t15_armstrng,t15_armstrng,t15_armstrng,t14_armstrng,t20_armstrng,d13_armstrng,t14_armstrng,d14_armstrng,d19_armstrng,t15_armstrng,t15_armstrng,t10_xboole_1,t1_xboole_1,d21_armstrng,t1_xboole_1,t15_armstrng,t10_xboole_1,t1_xboole_1,d21_armstrng,t1_xboole_1,t13_xboole_1,t15_armstrng,t10_armstrng,t19_armstrng,s1_xboole_0,d3_tarski,t13_finset_1,t1_xboole_1,t2_armstrng,d24_waybel_4,d24_waybel_4,t33_zfmisc_1,t14_armstrng,d24_waybel_4,d1_armstrng,t10_armstrng,d13_armstrng,t2_tarski]),
    [file(armstrng,t31_armstrng),interesting(0.37)]).

fof(t4_armstrng,theorem,(
    ! [A,B] : 
      ( ( ~ v1_xboole_0(B)
        & m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) )
     => ( v2_finsub_1(B)
       => ! [C] : 
            ( m2_subset_1(C,k1_zfmisc_1(A),B)
           => ( r1_armstrng(C,B)
             => ( C = A
                | ! [D] : 
                    ( ( v1_finset_1(D)
                      & m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(A))) )
                   => ( ( r1_tarski(D,B)
                        & C = k8_setfam_1(A,D) )
                     => r2_hidden(C,D) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t37_zfmisc_1,d10_setfam_1,t11_setfam_1,t8_xboole_1,t15_xboole_1,d10_setfam_1,d10_setfam_1,t10_setfam_1,d2_finsub_1,s2_finset_1,d2_armstrng,d10_setfam_1]),
    [file(armstrng,t4_armstrng),interesting(0.32)]).

fof(t6_armstrng,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1))
         => k3_armstrng(A,k6_binarith(A,k1_binari_3(A,0)),B) = B ) ) ),
    inference(mizar_proof,[status(thm)],[l1_armstrng,l1_armstrng,t26_binari_3,d4_euclid,l1_armstrng,t70_finseq_2,d4_finseq_4,d13_margrel1,d4_binarith,d16_margrel1,d5_armstrng,t50_margrel1,d4_finseq_4,t9_funct_1]),
    [file(armstrng,t6_armstrng),interesting(0.28)]).

fof(t47_armstrng,theorem,(
    ! [A,B,C] : 
      ( ( ~ v1_xboole_0(C)
        & v1_finset_1(C)
        & m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A))) )
     => ( ( v1_armstrng(C,A)
          & v2_finsub_1(C)
          & r5_armstrng(A,B,C) )
       => r1_tarski(k2_armstrng(C),k2_xboole_0(B,k1_tarski(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[d26_armstrng,d26_armstrng,d3_tarski,t1_xboole_1,t13_finset_1,t13_finset_1,d2_xboole_0,d1_tarski,d2_xboole_0,d3_armstrng,t4_armstrng]),
    [file(armstrng,t47_armstrng),interesting(0.27)]).

fof(t59_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ( ! [C] : 
                ( m1_subset_1(C,k1_zfmisc_1(A))
               => ! [D] : 
                    ( m1_subset_1(D,k1_zfmisc_1(A))
                   => ( r2_hidden(k6_armstrng(A,C,D),k12_armstrng(A,B))
                    <=> ! [E] : 
                          ( m1_subset_1(E,k1_zfmisc_1(A))
                         => ( r1_tarski(C,E)
                           => ( r1_tarski(D,E)
                              | r2_hidden(E,k14_armstrng(A,B)) ) ) ) ) ) )
            & k9_armstrng(A,k12_armstrng(A,B)) = k4_xboole_0(k1_zfmisc_1(A),k14_armstrng(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d25_armstrng,d4_xboole_0,t57_armstrng,d4_xboole_0,t2_tarski,t36_xboole_1,d4_subset_1,t57_armstrng,d4_xboole_0,d4_armstrng,t38_armstrng,t35_armstrng,t39_armstrng,d25_armstrng,t39_armstrng,d10_xboole_0,t33_zfmisc_1,d4_xboole_0,d4_xboole_0,t37_armstrng]),
    [file(armstrng,t59_armstrng),interesting(0.25)]).

fof(t48_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( ( v6_armstrng(B,A)
            & m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
         => ? [C] : 
              ( l1_armstrng(C)
              & u1_armstrng(C) = A
              & ! [D] : 
                  ( m1_subset_1(D,A)
                 => k1_funct_1(u2_armstrng(C),D) = k4_numbers )
              & B = k5_armstrng(C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_armstrng,d26_armstrng,t13_finset_1,t73_finseq_4,d4_finseq_1,d3_pboole,t19_funcop_1,t13_funcop_1,t17_numbers,t13_funcop_1,d5_card_3,d3_tarski,d1_tarski,d5_card_3,t13_funcop_1,d8_armstrng,d1_tarski,t2_tarski,t25_finseq_1,t60_relat_1,d3_finseq_1,d13_margrel1,d14_margrel1,s5_finseq_1,d11_finseq_1,d3_finseq_1,d4_finseq_2,s3_funct_2,t5_armstrng,t26_binari_3,t13_funcop_1,t7_binari_3,d3_tarski,t13_funcop_1,d8_armstrng,t18_card_3,t18_card_3,t90_relat_1,d3_xboole_0,l1_armstrng,l1_armstrng,l1_armstrng,t12_funct_1,d4_finseq_4,d5_armstrng,t49_margrel1,d13_margrel1,t49_margrel1,d13_margrel1,d5_armstrng,d3_tarski,l1_armstrng,d4_finseq_4,t72_funct_1,t72_funct_1,t50_margrel1,d14_margrel1,d5_armstrng,t2_binari_3,d5_armstrng,t50_margrel1,d14_margrel1,d5_armstrng,d5_armstrng,t9_funct_1,t70_funct_1,t68_funct_1,d3_tarski,t11_finseq_2,t3_finseq_1,t3_finseq_1,t22_nat_1,t38_nat_1,s4_funct_2,s4_funct_2,d1_funct_2,d3_pboole,t17_numbers,t13_funcop_1,d5_card_3,d1_funct_2,d3_pboole,t17_numbers,t13_funcop_1,d5_card_3,t90_relat_1,d3_xboole_0,t72_funct_1,l1_armstrng,l1_armstrng,l1_armstrng,t26_binari_3,d4_euclid,l1_armstrng,d4_finseq_4,t70_finseq_2,d5_armstrng,t49_margrel1,d13_margrel1,l1_armstrng,d4_finseq_4,t8_armstrng,d13_margrel1,d5_armstrng,t49_margrel1,d13_margrel1,l1_armstrng,d4_finseq_4,d5_armstrng,t49_margrel1,d13_margrel1,t9_funct_1,t68_funct_1,d8_armstrng,t72_funct_1,t72_funct_1,l1_armstrng,d4_finseq_4,t26_binari_3,d4_euclid,l1_armstrng,d4_finseq_4,t70_finseq_2,d5_armstrng,t50_margrel1,d14_margrel1,d5_armstrng,t50_margrel1,d14_margrel1,l1_armstrng,d4_finseq_4,t8_armstrng,t2_binari_3,t2_tarski]),
    [file(armstrng,t48_armstrng),interesting(0.22)]).

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(t11_armstrng,theorem,(
    $true ),
    file(armstrng,t11_armstrng),
    [interesting(0.00)]).

fof(t16_armstrng,theorem,(
    ! [A,B] : 
      ( r2_hidden(B,k7_armstrng(A))
    <=> ? [C] : 
          ( m1_subset_1(C,k4_armstrng(A))
          & ? [D] : 
              ( m1_subset_1(D,k4_armstrng(A))
              & B = k4_tarski(C,D)
              & r3_armstrng(A,D,C) ) ) ) ),
    file(armstrng,t16_armstrng),
    [interesting(0.00)]).

fof(t24_finset_1,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
    <=> v1_finset_1(k1_zfmisc_1(A)) ) ),
    file(finset_1,t24_finset_1),
    [interesting(0.00)]).

fof(t19_finset_1,theorem,(
    ! [A,B] : 
      ( ( v1_finset_1(A)
        & v1_finset_1(B) )
     => v1_finset_1(k2_zfmisc_1(A,B)) ) ),
    file(finset_1,t19_finset_1),
    [interesting(0.00)]).

fof(t13_finset_1,theorem,(
    ! [A,B] : 
      ( ( r1_tarski(A,B)
        & v1_finset_1(B) )
     => v1_finset_1(A) ) ),
    file(finset_1,t13_finset_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(d1_relset_1,definition,(
    ! [A,B,C] : 
      ( m1_relset_1(C,A,B)
    <=> r1_tarski(C,k2_zfmisc_1(A,B)) ) ),
    file(relset_1,d1_relset_1),
    [interesting(0.00)]).

fof(t33_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( k4_tarski(A,B) = k4_tarski(C,D)
     => ( A = C
        & B = D ) ) ),
    file(zfmisc_1,t33_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(d16_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v8_relat_2(A)
      <=> r8_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d16_relat_2),
    [interesting(0.00)]).

fof(t30_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r2_hidden(k4_tarski(A,B),C)
       => ( r2_hidden(A,k3_relat_1(C))
          & r2_hidden(B,k3_relat_1(C)) ) ) ) ),
    file(relat_1,t30_relat_1),
    [interesting(0.00)]).

fof(d8_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r8_relat_2(A,B)
        <=> ! [C,D,E] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(E,B)
                & r2_hidden(k4_tarski(C,D),A)
                & r2_hidden(k4_tarski(D,E),A) )
             => r2_hidden(k4_tarski(C,E),A) ) ) ) ),
    file(relat_2,d8_relat_2),
    [interesting(0.00)]).

fof(t19_relset_1,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => r1_tarski(k3_relat_1(C),k2_xboole_0(A,B)) ) ),
    file(relset_1,t19_relset_1),
    [interesting(0.00)]).

fof(t20_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v8_relat_2(B)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                        & r2_hidden(k6_armstrng(A,D,E),B) )
                     => r2_hidden(k6_armstrng(A,C,E),B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_relat_2,t30_relat_1,d8_relat_2,d8_relat_2,d16_relat_2,t19_relset_1]),
    [file(armstrng,t20_armstrng),interesting(0.00)]).

fof(d16_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v7_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ( r1_tarski(D,C)
                 => r2_hidden(k6_armstrng(A,C,D),B) ) ) ) ) ) ),
    file(armstrng,d16_armstrng),
    [interesting(0.00)]).

fof(t23_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( ( v7_armstrng(B,A)
          & v8_relat_2(B) )
       => ( v3_armstrng(B,A)
          & v4_armstrng(B,A) ) ) ) ),
    file(armstrng,t23_armstrng),
    [interesting(0.00)]).

fof(d15_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v6_armstrng(B,A)
      <=> ( v3_armstrng(B,A)
          & v8_relat_2(B)
          & v4_armstrng(B,A)
          & v5_armstrng(B,A) ) ) ) ),
    file(armstrng,d15_armstrng),
    [interesting(0.00)]).

fof(d14_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v5_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ! [F] : 
                        ( m1_subset_1(F,k1_zfmisc_1(A))
                       => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                            & r2_hidden(k6_armstrng(A,E,F),B) )
                         => r2_hidden(k6_armstrng(A,k4_subset_1(A,C,E),k4_subset_1(A,D,F)),B) ) ) ) ) ) ) ) ),
    file(armstrng,d14_armstrng),
    [interesting(0.00)]).

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

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

fof(t27_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => r1_tarski(k8_armstrng(A,B),B) ) ),
    file(armstrng,t27_armstrng),
    [interesting(0.00)]).

fof(t80_zfmisc_1,theorem,(
    ! [A] : r1_tarski(k1_tarski(A),k1_zfmisc_1(A)) ),
    file(zfmisc_1,t80_zfmisc_1),
    [interesting(0.00)]).

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

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

fof(d4_armstrng,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( v1_armstrng(B,A)
      <=> r2_hidden(A,B) ) ) ),
    file(armstrng,d4_armstrng),
    [interesting(0.00)]).

fof(d2_finsub_1,definition,(
    ! [A] : 
      ( v2_finsub_1(A)
    <=> ! [B,C] : 
          ( ( r2_hidden(B,A)
            & r2_hidden(C,A) )
         => r2_hidden(k3_xboole_0(B,C),A) ) ) ),
    file(finsub_1,d2_finsub_1),
    [interesting(0.00)]).

fof(t28_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => k3_xboole_0(A,B) = A ) ),
    file(xboole_1,t28_xboole_1),
    [interesting(0.00)]).

fof(t18_xboole_1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(A,k3_xboole_0(B,C))
     => r1_tarski(A,B) ) ),
    file(xboole_1,t18_xboole_1),
    [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(d1_eqrel_1,definition,(
    ! [A] : k1_eqrel_1(A) = k2_zfmisc_1(A,A) ),
    file(eqrel_1,d1_eqrel_1),
    [interesting(0.00)]).

fof(t97_orders_1,theorem,(
    ! [A,B] : 
      ( ( v1_partfun1(B,A,A)
        & m2_relset_1(B,A,A) )
     => k3_relat_1(B) = A ) ),
    file(orders_1,t97_orders_1),
    [interesting(0.00)]).

fof(d12_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v3_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => r2_hidden(k6_armstrng(A,C,C),B) ) ) ) ),
    file(armstrng,d12_armstrng),
    [interesting(0.00)]).

fof(d13_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v4_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ! [F] : 
                        ( m1_subset_1(F,k1_zfmisc_1(A))
                       => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                            & r3_armstrng(A,k6_armstrng(A,C,D),k6_armstrng(A,E,F)) )
                         => r2_hidden(k6_armstrng(A,E,F),B) ) ) ) ) ) ) ) ),
    file(armstrng,d13_armstrng),
    [interesting(0.00)]).

fof(d1_mcart_1,definition,(
    ! [A] : 
      ( ? [B,C] : A = k4_tarski(B,C)
     => ! [B] : 
          ( B = k1_mcart_1(A)
        <=> ! [C,D] : 
              ( A = k4_tarski(C,D)
             => B = C ) ) ) ),
    file(mcart_1,d1_mcart_1),
    [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(d10_armstrng,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k4_armstrng(A))
     => ! [C] : 
          ( m1_subset_1(C,k4_armstrng(A))
         => ( r3_armstrng(A,B,C)
          <=> ( r1_tarski(k1_mcart_1(B),k1_mcart_1(C))
              & r1_tarski(k2_mcart_1(C),k2_mcart_1(B)) ) ) ) ) ),
    file(armstrng,d10_armstrng),
    [interesting(0.00)]).

fof(t11_xboole_1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(k2_xboole_0(A,B),C)
     => r1_tarski(A,C) ) ),
    file(xboole_1,t11_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(d19_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v8_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ? [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
                & ? [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                    & r3_armstrng(A,k6_armstrng(A,D,E),k6_armstrng(A,C,C))
                    & r2_hidden(k6_armstrng(A,D,E),B) ) ) ) ) ) ),
    file(armstrng,d19_armstrng),
    [interesting(0.00)]).

fof(d6_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => k3_relat_1(A) = k2_xboole_0(k1_relat_1(A),k2_relat_1(A)) ) ),
    file(relat_1,d6_relat_1),
    [interesting(0.00)]).

fof(d4_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( B = k1_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : r2_hidden(k4_tarski(C,D),A) ) ) ) ),
    file(relat_1,d4_relat_1),
    [interesting(0.00)]).

fof(d5_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_1,d5_relat_1),
    [interesting(0.00)]).

fof(s1_xboole_0,theorem,(
    ? [A] : 
    ! [B] : 
      ( r2_hidden(B,A)
    <=> ( r2_hidden(B,f1_s1_xboole_0)
        & p1_s1_xboole_0(B) ) ) ),
    file(xboole_0,s1_xboole_0),
    [interesting(0.00)]).

fof(t4_polynom1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(k3_relat_1(B),A)
       => m2_relset_1(B,A,A) ) ) ),
    file(polynom1,t4_polynom1),
    [interesting(0.00)]).

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

fof(d12_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v4_relat_2(A)
      <=> r4_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d12_relat_2),
    [interesting(0.00)]).

fof(d3_yellow_0,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v4_orders_2(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( ( r1_orders_2(A,B,C)
                    & r1_orders_2(A,C,B) )
                 => B = C ) ) ) ) ) ),
    file(yellow_0,d3_yellow_0),
    [interesting(0.00)]).

fof(d9_orders_2,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r1_orders_2(A,B,C)
              <=> r2_hidden(k4_tarski(B,C),u1_orders_2(A)) ) ) ) ) ),
    file(orders_2,d9_orders_2),
    [interesting(0.00)]).

fof(d4_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r4_relat_2(A,B)
        <=> ! [C,D] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(k4_tarski(C,D),A)
                & r2_hidden(k4_tarski(D,C),A) )
             => C = D ) ) ) ),
    file(relat_2,d4_relat_2),
    [interesting(0.00)]).

fof(d2_yellow_0,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v3_orders_2(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( ( r1_orders_2(A,B,C)
                        & r1_orders_2(A,C,D) )
                     => r1_orders_2(A,B,D) ) ) ) ) ) ) ),
    file(yellow_0,d2_yellow_0),
    [interesting(0.00)]).

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

fof(t7_bagorder,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_orders_2(A)
        & v4_orders_2(A)
        & l1_orders_2(A) )
     => ! [B] : 
          ( ( v1_finset_1(B)
            & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
         => ~ ( B != k1_xboole_0
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( r2_hidden(C,B)
                      & r2_waybel_4(B,C,u1_orders_2(A)) ) ) ) ) ) ),
    file(bagorder,t7_bagorder),
    [interesting(0.00)]).

fof(d24_waybel_4,definition,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r2_waybel_4(A,B,C)
      <=> ( r2_hidden(B,A)
          & ! [D] : ~ ( r2_hidden(D,A)
              & D != B
              & r2_hidden(k4_tarski(B,D),C) ) ) ) ) ),
    file(waybel_4,d24_waybel_4),
    [interesting(0.00)]).

fof(d1_armstrng,definition,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( C = k1_armstrng(A,B)
          <=> ! [D] : 
                ( r2_hidden(D,C)
              <=> r2_waybel_4(A,D,B) ) ) ) ) ),
    file(armstrng,d1_armstrng),
    [interesting(0.00)]).

fof(d20_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v9_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ! [F] : 
                        ( m1_subset_1(F,k1_zfmisc_1(A))
                       => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                            & r2_hidden(k6_armstrng(A,E,F),B)
                            & r3_armstrng(A,k6_armstrng(A,C,D),k6_armstrng(A,E,F)) )
                         => ( C = E
                            & D = F ) ) ) ) ) ) ) ) ),
    file(armstrng,d20_armstrng),
    [interesting(0.00)]).

fof(d21_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v10_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ! [F] : 
                        ( m1_subset_1(F,k1_zfmisc_1(A))
                       => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                            & r2_hidden(k6_armstrng(A,E,F),B)
                            & r1_tarski(E,D) )
                         => r1_tarski(F,D) ) ) ) ) ) ) ) ),
    file(armstrng,d21_armstrng),
    [interesting(0.00)]).

fof(d18_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ! [C,D] : 
          ( r4_armstrng(A,B,C,D)
        <=> r2_hidden(k4_tarski(C,D),k8_armstrng(A,B)) ) ) ),
    file(armstrng,d18_armstrng),
    [interesting(0.00)]).

fof(t6_relset_1,theorem,(
    ! [A,B,C,D] : 
      ( m2_relset_1(D,A,B)
     => ~ ( r2_hidden(C,D)
          & ! [E,F] : ~ ( C = k4_tarski(E,F)
              & r2_hidden(E,A)
              & r2_hidden(F,B) ) ) ) ),
    file(relset_1,t6_relset_1),
    [interesting(0.00)]).

fof(t29_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ! [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(A))
             => ( r4_armstrng(A,B,C,D)
              <=> ( r2_hidden(k6_armstrng(A,C,D),B)
                  & ! [E] : 
                      ( m1_subset_1(E,k1_zfmisc_1(A))
                     => ! [F] : 
                          ( m1_subset_1(F,k1_zfmisc_1(A))
                         => ~ ( r2_hidden(k6_armstrng(A,E,F),B)
                              & ~ ( C = E
                                  & D = F )
                              & r3_armstrng(A,k6_armstrng(A,E,F),k6_armstrng(A,C,D)) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_armstrng,d1_armstrng,t33_zfmisc_1,d24_waybel_4,d24_waybel_4,t6_relset_1,t33_zfmisc_1,d1_armstrng,d18_armstrng]),
    [file(armstrng,t29_armstrng),interesting(0.00)]).

fof(t7_xboole_1,theorem,(
    ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ),
    file(xboole_1,t7_xboole_1),
    [interesting(0.00)]).

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

fof(t33_armstrng,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( r2_hidden(B,k9_armstrng(A,C))
      <=> ? [D] : 
            ( m1_subset_1(D,k1_zfmisc_1(A))
            & ? [E] : 
                ( m1_subset_1(E,k1_zfmisc_1(A))
                & B = D
                & r4_armstrng(A,C,E,D) ) ) ) ) ),
    file(armstrng,t33_armstrng),
    [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(d10_setfam_1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( ( B != k1_xboole_0
         => k8_setfam_1(A,B) = k6_setfam_1(A,B) )
        & ( B = k1_xboole_0
         => k8_setfam_1(A,B) = A ) ) ) ),
    file(setfam_1,d10_setfam_1),
    [interesting(0.00)]).

fof(t4_setfam_1,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => r1_tarski(k1_setfam_1(B),A) ) ),
    file(setfam_1,t4_setfam_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(t8_mssubfam,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ! [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(A)))
             => ( B = k4_subset_1(k1_zfmisc_1(A),C,D)
               => k8_setfam_1(A,B) = k5_subset_1(A,k8_setfam_1(A,C),k8_setfam_1(A,D)) ) ) ) ) ),
    file(mssubfam,t8_mssubfam),
    [interesting(0.00)]).

fof(t9_mssubfam,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( B = k1_tarski(C)
           => k8_setfam_1(A,B) = C ) ) ) ),
    file(mssubfam,t9_mssubfam),
    [interesting(0.00)]).

fof(s2_finset_1,theorem,
    ( ( v1_finset_1(f1_s2_finset_1)
      & p1_s2_finset_1(k1_xboole_0)
      & ! [A,B] : 
          ( ( r2_hidden(A,f1_s2_finset_1)
            & r1_tarski(B,f1_s2_finset_1)
            & p1_s2_finset_1(B) )
         => p1_s2_finset_1(k2_xboole_0(B,k1_tarski(A))) ) )
   => p1_s2_finset_1(f1_s2_finset_1) ),
    file(finset_1,s2_finset_1),
    [interesting(0.00)]).

fof(t102_zfmisc_1,theorem,(
    ! [A,B,C] : ~ ( r2_hidden(A,k2_zfmisc_1(B,C))
      & ! [D,E] : k4_tarski(D,E) != A ) ),
    file(zfmisc_1,t102_zfmisc_1),
    [interesting(0.00)]).

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

fof(t28_armstrng,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m1_subset_1(B,k4_armstrng(A))
         => ! [C] : 
              ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
             => ~ ( r2_hidden(B,C)
                  & ! [D] : 
                      ( m1_subset_1(D,k1_zfmisc_1(A))
                     => ! [E] : 
                          ( m1_subset_1(E,k1_zfmisc_1(A))
                         => ~ ( r2_hidden(k6_armstrng(A,D,E),k8_armstrng(A,C))
                              & r3_armstrng(A,k6_armstrng(A,D,E),B) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_armstrng,d3_tarski,t13_finset_1,t2_armstrng,d24_waybel_4,t9_armstrng,d24_waybel_4,t33_zfmisc_1,t14_armstrng,d24_waybel_4,d1_armstrng]),
    [file(armstrng,t28_armstrng),interesting(0.00)]).

fof(d4_subset_1,definition,(
    ! [A] : k2_subset_1(A) = A ),
    file(subset_1,d4_subset_1),
    [interesting(0.00)]).

fof(t24_mcart_1,theorem,(
    ! [A,B] : ~ ( A != k1_xboole_0
      & B != k1_xboole_0
      & ~ ! [C] : 
            ( m1_subset_1(C,k2_zfmisc_1(A,B))
           => C = k4_tarski(k1_mcart_1(C),k2_mcart_1(C)) ) ) ),
    file(mcart_1,t24_mcart_1),
    [interesting(0.00)]).

fof(t17_xboole_1,theorem,(
    ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ),
    file(xboole_1,t17_xboole_1),
    [interesting(0.00)]).

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

fof(d26_armstrng,definition,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( r5_armstrng(A,B,C)
      <=> ( r1_tarski(B,C)
          & C = a_2_11_armstrng(A,B) ) ) ) ),
    file(armstrng,d26_armstrng),
    [interesting(0.00)]).

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

fof(t2_mssubfam,theorem,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( r2_hidden(B,C)
       => r1_tarski(k8_setfam_1(A,C),B) ) ) ),
    file(mssubfam,t2_mssubfam),
    [interesting(0.00)]).

fof(d2_armstrng,definition,(
    ! [A,B] : 
      ( r1_armstrng(A,B)
    <=> ( r2_hidden(A,B)
        & ! [C,D] : ~ ( r2_hidden(C,B)
            & r2_hidden(D,B)
            & A = k3_xboole_0(C,D)
            & A != C
            & A != D ) ) ) ),
    file(armstrng,d2_armstrng),
    [interesting(0.00)]).

fof(t11_setfam_1,theorem,(
    ! [A] : k1_setfam_1(k1_tarski(A)) = A ),
    file(setfam_1,t11_setfam_1),
    [interesting(0.00)]).

fof(t10_setfam_1,theorem,(
    ! [A,B] : ~ ( A != k1_xboole_0
      & B != k1_xboole_0
      & k1_setfam_1(k2_xboole_0(A,B)) != k3_xboole_0(k1_setfam_1(A),k1_setfam_1(B)) ) ),
    file(setfam_1,t10_setfam_1),
    [interesting(0.00)]).

fof(s5_nat_1,theorem,
    ( ? [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
        & p1_s5_nat_1(A) )
   => ? [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
        & p1_s5_nat_1(A)
        & ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( p1_s5_nat_1(B)
             => r1_xreal_0(A,B) ) ) ) ),
    file(nat_1,s5_nat_1),
    [interesting(0.00)]).

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

fof(t24_trees_1,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( v1_finset_1(B)
         => ~ ( r2_xboole_0(A,B)
              & r1_xreal_0(k4_card_1(B),k4_card_1(A)) ) ) ) ),
    file(trees_1,t24_trees_1),
    [interesting(0.00)]).

fof(d3_armstrng,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ( B = k2_armstrng(A)
          <=> ! [C] : 
                ( r2_hidden(C,B)
              <=> r1_armstrng(C,A) ) ) ) ) ),
    file(armstrng,d3_armstrng),
    [interesting(0.00)]).

fof(t15_xboole_1,theorem,(
    ! [A,B] : 
      ( k2_xboole_0(A,B) = k1_xboole_0
     => A = k1_xboole_0 ) ),
    file(xboole_1,t15_xboole_1),
    [interesting(0.00)]).

fof(t73_finseq_4,theorem,(
    ! [A] : ~ ( v1_finset_1(A)
      & ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ~ ( k2_relat_1(B) = A
              & v2_funct_1(B) ) ) ) ),
    file(finseq_4,t73_finseq_4),
    [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(d3_pboole,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( m1_pboole(B,A)
      <=> k1_relat_1(B) = A ) ) ),
    file(pboole,d3_pboole),
    [interesting(0.00)]).

fof(t19_funcop_1,theorem,(
    ! [A,B] : 
      ( k1_relat_1(k2_funcop_1(A,B)) = A
      & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ),
    file(funcop_1,t19_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(t17_numbers,theorem,(
    r1_tarski(k5_numbers,k4_numbers) ),
    file(numbers,t17_numbers),
    [interesting(0.00)]).

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

fof(d8_armstrng,definition,(
    ! [A] : 
      ( l1_armstrng(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_armstrng(A)))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(u1_armstrng(A)))
             => ( r2_armstrng(A,B,C)
              <=> ! [D] : 
                    ( m1_subset_1(D,u3_armstrng(A))
                   => ! [E] : 
                        ( m1_subset_1(E,u3_armstrng(A))
                       => ( k7_relat_1(D,B) = k7_relat_1(E,B)
                         => k7_relat_1(D,C) = k7_relat_1(E,C) ) ) ) ) ) ) ) ),
    file(armstrng,d8_armstrng),
    [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(t60_relat_1,theorem,
    ( k1_relat_1(k1_xboole_0) = k1_xboole_0
    & k2_relat_1(k1_xboole_0) = k1_xboole_0 ),
    file(relat_1,t60_relat_1),
    [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(d13_margrel1,definition,(
    k7_margrel1 = 0 ),
    file(margrel1,d13_margrel1),
    [interesting(0.00)]).

fof(d14_margrel1,definition,(
    k8_margrel1 = 1 ),
    file(margrel1,d14_margrel1),
    [interesting(0.00)]).

fof(s5_finseq_1,theorem,
    ( ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ~ ( r2_hidden(A,k2_finseq_1(f2_s5_finseq_1))
            & ! [B] : 
                ( m1_subset_1(B,f1_s5_finseq_1)
               => ~ p1_s5_finseq_1(A,B) ) ) )
   => ? [A] : 
        ( m2_finseq_1(A,f1_s5_finseq_1)
        & k4_finseq_1(A) = k2_finseq_1(f2_s5_finseq_1)
        & ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( r2_hidden(B,k2_finseq_1(f2_s5_finseq_1))
             => p1_s5_finseq_1(B,k1_funct_1(A,B)) ) ) ) ),
    file(finseq_1,s5_finseq_1),
    [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(d4_finseq_2,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k4_finseq_2(A,B) = a_2_0_finseq_2(A,B) ) ),
    file(finseq_2,d4_finseq_2),
    [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(t109_finseq_2,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_2(C,B,k4_finseq_2(A,B))
             => k3_finseq_1(C) = A ) ) ) ),
    file(finseq_2,t109_finseq_2),
    [interesting(0.00)]).

fof(t26_binari_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => k1_binari_3(A,0) = k5_euclid(A) ) ),
    file(binari_3,t26_binari_3),
    [interesting(0.00)]).

fof(d4_euclid,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => k4_euclid(A) = k4_finseqop(k1_numbers,A,0) ) ),
    file(euclid,d4_euclid),
    [interesting(0.00)]).

fof(t70_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B,C] : 
          ( r2_hidden(B,k2_finseq_1(A))
         => k1_funct_1(k2_finseq_2(A,C),B) = C ) ) ),
    file(finseq_2,t70_finseq_2),
    [interesting(0.00)]).

fof(d4_finseq_4,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( r2_hidden(D,k1_relat_1(C))
         => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ),
    file(finseq_4,d4_finseq_4),
    [interesting(0.00)]).

fof(d5_armstrng,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1))
         => ! [C] : 
              ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1))
             => ! [D] : 
                  ( m2_finseq_2(D,k6_margrel1,k4_finseq_2(A,k6_margrel1))
                 => ( D = k3_armstrng(A,B,C)
                  <=> ! [E] : 
                        ( r2_hidden(E,k2_finseq_1(A))
                       => k1_funct_1(D,E) = k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,E),k4_finseq_4(k5_numbers,k6_margrel1,C,E)) ) ) ) ) ) ) ),
    file(armstrng,d5_armstrng),
    [interesting(0.00)]).

fof(t49_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(k7_margrel1,A) = k7_margrel1 ) ),
    file(margrel1,t49_margrel1),
    [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(t7_binari_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & m2_subset_1(A,k1_numbers,k5_numbers) )
     => ! [B] : 
          ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1))
         => ( B = k5_euclid(A)
           => k9_binarith(A,B) = 0 ) ) ) ),
    file(binari_3,t7_binari_3),
    [interesting(0.00)]).

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

fof(t90_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => k1_relat_1(k7_relat_1(B,A)) = k3_xboole_0(k1_relat_1(B),A) ) ),
    file(relat_1,t90_relat_1),
    [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(t12_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( r2_hidden(A,k1_relat_1(B))
       => r2_hidden(k1_funct_1(B,A),k2_relat_1(B)) ) ) ),
    file(funct_1,t12_funct_1),
    [interesting(0.00)]).

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

fof(t50_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(k8_margrel1,A) = A ) ),
    file(margrel1,t50_margrel1),
    [interesting(0.00)]).

fof(t2_binari_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & m2_subset_1(A,k1_numbers,k5_numbers) )
     => ! [B] : 
          ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1))
         => ! [C] : 
              ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1))
             => ( k9_binarith(A,B) = k9_binarith(A,C)
               => B = C ) ) ) ) ),
    file(binari_3,t2_binari_3),
    [interesting(0.00)]).

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

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

fof(t11_finseq_2,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ~ ( r2_hidden(A,k2_relat_1(B))
          & ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ~ ( r2_hidden(C,k4_finseq_1(B))
                  & k1_funct_1(B,C) = A ) ) ) ) ),
    file(finseq_2,t11_finseq_2),
    [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(t22_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ~ ( A != 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => A != k1_nat_1(B,1) ) ) ) ),
    file(nat_1,t22_nat_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(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(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(t68_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k4_finseq_1(k2_finseq_2(A,B)) = k2_finseq_1(A) ) ),
    file(finseq_2,t68_finseq_2),
    [interesting(0.00)]).

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

fof(t29_binari_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => k1_binari_3(k1_nat_1(A,1),k3_series_1(2,A)) = k8_finseq_1(k1_numbers,k5_euclid(A),k13_binarith(k1_numbers,1)) ) ),
    file(binari_3,t29_binari_3),
    [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(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(t44_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(B,A)
                  & ~ r1_xreal_0(C,1)
                  & r1_xreal_0(k3_power(C,B),k3_power(C,A)) ) ) ) ) ),
    file(power,t44_power),
    [interesting(0.00)]).

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

fof(t28_binari_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & m2_subset_1(A,k1_numbers,k5_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ~ r1_xreal_0(k3_series_1(2,A),B)
           => k1_binari_3(k1_nat_1(A,1),B) = k12_binarith(A,1,k6_margrel1,k1_binari_3(A,B),k13_binarith(k6_margrel1,k7_margrel1)) ) ) ) ),
    file(binari_3,t28_binari_3),
    [interesting(0.00)]).

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

fof(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(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(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(d4_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( ( r2_hidden(B,k1_relat_1(A))
           => ( C = k1_funct_1(A,B)
            <=> r2_hidden(k4_tarski(B,C),A) ) )
          & ( ~ r2_hidden(B,k1_relat_1(A))
           => ( C = k1_funct_1(A,B)
            <=> C = k1_xboole_0 ) ) ) ) ),
    file(funct_1,d4_funct_1),
    [interesting(0.00)]).

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

fof(t27_binari_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ~ r1_xreal_0(k3_series_1(2,A),B)
           => k1_funct_1(k1_binari_3(k1_nat_1(A,1),B),k1_nat_1(A,1)) = k7_margrel1 ) ) ) ),
    file(binari_3,t27_binari_3),
    [interesting(0.00)]).

fof(t8_armstrng,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ~ r1_xreal_0(A,B)
           => ( k1_funct_1(k1_binari_3(A,k3_series_1(2,B)),k1_nat_1(B,1)) = 1
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( r2_hidden(C,k2_finseq_1(A))
                   => ( C = k1_nat_1(B,1)
                      | k1_funct_1(k1_binari_3(A,k3_series_1(2,B)),C) = 0 ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_nat_1,d4_euclid,t68_finseq_2,d3_finseq_1,t55_finseq_1,t3_finseq_1,t29_binari_3,d14_margrel1,d7_finseq_1,t57_finseq_1,d4_euclid,t68_finseq_2,d3_finseq_1,t55_finseq_1,t3_finseq_1,t29_binari_3,d14_margrel1,d7_finseq_1,t57_finseq_1,t44_power,t8_xreal_1,t38_nat_1,t3_finseq_1,l1_armstrng,t28_binari_3,d7_finseq_1,d5_real_1,s1_nat_1,t38_nat_1,t8_xreal_1,l1_armstrng,t2_xreal_1,t1_xreal_1,t3_finseq_1,d4_funct_1,d13_margrel1,l1_armstrng,t38_nat_1,t3_finseq_1,d4_funct_1,d13_margrel1,t44_power,d5_real_1,t38_nat_1,l1_armstrng,t38_nat_1,t3_finseq_1,d4_funct_1,d13_margrel1,l1_armstrng,d3_finseq_1,t55_finseq_1,t3_finseq_1,t28_binari_3,d7_finseq_1,t57_finseq_1,t37_nat_1,t38_nat_1,t3_finseq_1,l1_armstrng,t28_binari_3,d7_finseq_1,d5_real_1,d5_real_1,s1_nat_1,t38_nat_1,t38_nat_1,l1_armstrng,t38_nat_1,t2_xreal_1,t3_finseq_1,t44_power,t28_binari_3,d7_finseq_1,t38_nat_1,t3_finseq_1,d4_euclid,t68_finseq_2,t29_binari_3,d14_margrel1,d7_finseq_1,t70_finseq_2,d13_margrel1,d5_real_1,s1_nat_1,d14_margrel1,t3_finseq_1,d13_margrel1,t22_nat_1,t38_nat_1,t38_nat_1,d13_margrel1,t22_nat_1,t8_xreal_1,t44_power,t27_binari_3,d13_margrel1,d5_real_1]),
    [file(armstrng,t8_armstrng),interesting(0.00)]).

fof(t103_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r1_tarski(A,B)
       => k7_relat_1(k7_relat_1(C,B),A) = k7_relat_1(C,A) ) ) ),
    file(relat_1,t103_relat_1),
    [interesting(0.00)]).

fof(t107_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => k7_relat_1(C,k2_xboole_0(A,B)) = k2_xboole_0(k7_relat_1(C,A),k7_relat_1(C,B)) ) ),
    file(relat_1,t107_relat_1),
    [interesting(0.00)]).

fof(d28_armstrng,definition,(
    ! [A] : 
      ( v11_armstrng(A)
    <=> ! [B,C] : 
          ( ( r2_hidden(B,A)
            & r2_hidden(C,A)
            & r1_tarski(B,C) )
         => B = C ) ) ),
    file(armstrng,d28_armstrng),
    [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_funct_4,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C) )
             => ( C = k1_funct_4(A,B)
              <=> ( k1_relat_1(C) = k2_xboole_0(k1_relat_1(A),k1_relat_1(B))
                  & ! [D] : 
                      ( r2_hidden(D,k2_xboole_0(k1_relat_1(A),k1_relat_1(B)))
                     => ( ( r2_hidden(D,k1_relat_1(B))
                         => k1_funct_1(C,D) = k1_funct_1(B,D) )
                        & ( ~ r2_hidden(D,k1_relat_1(B))
                         => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) ) ) ) ) ) ) ),
    file(funct_4,d1_funct_4),
    [interesting(0.00)]).

fof(t12_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => k2_xboole_0(A,B) = B ) ),
    file(xboole_1,t12_xboole_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(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(t16_funcop_1,theorem,(
    ! [A] : 
      ( k1_relat_1(k2_funcop_1(k1_xboole_0,A)) = k1_xboole_0
      & k2_relat_1(k2_funcop_1(k1_xboole_0,A)) = k1_xboole_0 ) ),
    file(funcop_1,t16_funcop_1),
    [interesting(0.00)]).

fof(t64_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( ( k1_relat_1(A) = k1_xboole_0
          | k2_relat_1(A) = k1_xboole_0 )
       => A = k1_xboole_0 ) ) ),
    file(relat_1,t64_relat_1),
    [interesting(0.00)]).

fof(t22_funct_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => k1_funct_4(A,k1_xboole_0) = A ) ),
    file(funct_4,t22_funct_4),
    [interesting(0.00)]).

fof(d7_xboole_0,definition,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
    <=> k3_xboole_0(A,B) = k1_xboole_0 ) ),
    file(xboole_0,d7_xboole_0),
    [interesting(0.00)]).

fof(t44_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( r1_xboole_0(B,k3_subset_1(A,C))
          <=> r1_tarski(B,C) ) ) ) ),
    file(subset_1,t44_subset_1),
    [interesting(0.00)]).

fof(t26_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => r1_xboole_0(B,k3_subset_1(A,B)) ) ),
    file(subset_1,t26_subset_1),
    [interesting(0.00)]).

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

fof(t39_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ( r1_tarski(k3_subset_1(A,B),B)
      <=> B = k2_subset_1(A) ) ) ),
    file(subset_1,t39_subset_1),
    [interesting(0.00)]).

fof(t24_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( ( v3_armstrng(B,A)
          & v4_armstrng(B,A) )
       => v7_armstrng(B,A) ) ) ),
    file(armstrng,t24_armstrng),
    [interesting(0.00)]).

fof(t54_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( ( ( v3_armstrng(B,A)
            & v8_relat_2(B)
            & v4_armstrng(B,A)
            & v5_armstrng(B,A) )
         => ( v8_relat_2(B)
            & v7_armstrng(B,A)
            & v5_armstrng(B,A) ) )
        & ( ( v8_relat_2(B)
            & v7_armstrng(B,A)
            & v5_armstrng(B,A) )
         => ( v3_armstrng(B,A)
            & v8_relat_2(B)
            & v4_armstrng(B,A)
            & v5_armstrng(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_armstrng,t24_armstrng]),
    [file(armstrng,t54_armstrng),interesting(0.00)]).

fof(d29_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v12_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                        & r2_hidden(k6_armstrng(A,C,E),B) )
                     => r2_hidden(k6_armstrng(A,C,k4_subset_1(A,D,E)),B) ) ) ) ) ) ) ),
    file(armstrng,d29_armstrng),
    [interesting(0.00)]).

fof(t55_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( ( ( v3_armstrng(B,A)
            & v8_relat_2(B)
            & v4_armstrng(B,A)
            & v5_armstrng(B,A) )
         => ( v8_relat_2(B)
            & v7_armstrng(B,A)
            & v12_armstrng(B,A) ) )
        & ( ( v8_relat_2(B)
            & v7_armstrng(B,A)
            & v12_armstrng(B,A) )
         => ( v3_armstrng(B,A)
            & v8_relat_2(B)
            & v4_armstrng(B,A)
            & v5_armstrng(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_armstrng,d29_armstrng,d14_armstrng,t23_armstrng,t23_armstrng,d14_armstrng,t7_xboole_1,d16_armstrng,t20_armstrng,d29_armstrng]),
    [file(armstrng,t55_armstrng),interesting(0.00)]).

fof(d30_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v13_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ! [F] : 
                        ( m1_subset_1(F,k1_zfmisc_1(A))
                       => ( ( r2_hidden(k6_armstrng(A,C,D),B)
                            & r2_hidden(k6_armstrng(A,k4_subset_1(A,D,E),F),B) )
                         => r2_hidden(k6_armstrng(A,k4_subset_1(A,C,E),F),B) ) ) ) ) ) ) ) ),
    file(armstrng,d30_armstrng),
    [interesting(0.00)]).

fof(d31_armstrng,definition,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( v14_armstrng(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,k1_zfmisc_1(A))
           => ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ! [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                   => ( r2_hidden(k6_armstrng(A,C,D),B)
                     => r2_hidden(k6_armstrng(A,k4_subset_1(A,C,E),D),B) ) ) ) ) ) ) ),
    file(armstrng,d31_armstrng),
    [interesting(0.00)]).

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

fof(t56_armstrng,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( ( ( v3_armstrng(B,A)
            & v8_relat_2(B)
            & v4_armstrng(B,A)
            & v5_armstrng(B,A) )
         => ( v3_armstrng(B,A)
            & v13_armstrng(B,A)
            & v14_armstrng(B,A) ) )
        & ( ( v3_armstrng(B,A)
            & v13_armstrng(B,A)
            & v14_armstrng(B,A) )
         => ( v3_armstrng(B,A)
            & v8_relat_2(B)
            & v4_armstrng(B,A)
            & v5_armstrng(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d30_armstrng,d12_armstrng,d14_armstrng,t20_armstrng,d31_armstrng,t24_armstrng,t7_xboole_1,d16_armstrng,t20_armstrng,d31_armstrng,d30_armstrng,t20_armstrng,d13_armstrng,t15_armstrng,t45_xboole_1,d31_armstrng,d12_armstrng,t45_xboole_1,d31_armstrng,d14_armstrng,d12_armstrng,d30_armstrng,d30_armstrng]),
    [file(armstrng,t56_armstrng),interesting(0.00)]).

fof(t58_armstrng,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ( ? [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
                & ? [E] : 
                    ( m1_subset_1(E,k1_zfmisc_1(A))
                    & r2_hidden(k6_armstrng(A,D,E),C)
                    & r1_tarski(D,B)
                    & ~ r1_tarski(E,B) ) )
           => r2_hidden(B,k14_armstrng(A,C)) ) ) ) ),
    file(armstrng,t58_armstrng),
    [interesting(0.00)]).

fof(d25_armstrng,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ! [C] : 
              ( ( v6_armstrng(C,A)
                & m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A)) )
             => ( C = k12_armstrng(A,B)
              <=> ( r1_tarski(B,C)
                  & ! [D] : 
                      ( m2_relset_1(D,k1_zfmisc_1(A),k1_zfmisc_1(A))
                     => ( ( r1_tarski(B,D)
                          & v6_armstrng(D,A) )
                       => r1_tarski(C,D) ) ) ) ) ) ) ) ),
    file(armstrng,d25_armstrng),
    [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(t57_armstrng,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( r2_hidden(B,k14_armstrng(A,C))
       => ( m1_subset_1(B,k1_zfmisc_1(A))
          & ? [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(A))
              & ? [E] : 
                  ( m1_subset_1(E,k1_zfmisc_1(A))
                  & r2_hidden(k6_armstrng(A,D,E),C)
                  & r1_tarski(D,B)
                  & ~ r1_tarski(E,B) ) ) ) ) ) ),
    file(armstrng,t57_armstrng),
    [interesting(0.00)]).

fof(t36_xboole_1,theorem,(
    ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ),
    file(xboole_1,t36_xboole_1),
    [interesting(0.00)]).

fof(t39_armstrng,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A) )
     => ! [B] : 
          ( m2_relset_1(B,k1_zfmisc_1(A),k1_zfmisc_1(A))
         => ( r1_tarski(B,k10_armstrng(A,k11_armstrng(A,B)))
            & ! [C] : 
                ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
               => ( ( r1_tarski(B,C)
                    & v6_armstrng(C,A) )
                 => r1_tarski(k10_armstrng(A,k11_armstrng(A,B)),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t10_armstrng,d3_tarski,t38_armstrng,t37_armstrng,t34_armstrng,t37_armstrng,d3_tarski,t33_zfmisc_1]),
    [file(armstrng,t39_armstrng),interesting(0.00)]).

fof(d33_armstrng,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,k1_zfmisc_1(A),k1_zfmisc_1(A))
     => ( r6_armstrng(A,B,C)
      <=> ( ! [D] : 
              ( m1_subset_1(D,k1_zfmisc_1(A))
             => ( r1_tarski(B,D)
               => ( D = A
                  | r2_hidden(D,k14_armstrng(A,C)) ) ) )
          & ! [D] : ~ ( r2_xboole_0(D,B)
              & ! [E] : 
                  ( m1_subset_1(E,k1_zfmisc_1(A))
                 => ~ ( r1_tarski(D,E)
                      & E != A
                      & ~ r2_hidden(E,k14_armstrng(A,C)) ) ) ) ) ) ) ),
    file(armstrng,d33_armstrng),
    [interesting(0.00)]).

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

fof(d4_binarith,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1))
         => ! [C] : 
              ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1))
             => ( C = k6_binarith(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => ( r2_hidden(D,k2_finseq_1(A))
                     => k4_finseq_4(k5_numbers,k6_margrel1,C,D) = k11_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,D)) ) ) ) ) ) ) ),
    file(binarith,d4_binarith),
    [interesting(0.00)]).

fof(d16_margrel1,definition,(
    ! [A] : 
      ( v2_margrel1(A)
     => ( ( A = k7_margrel1
         => k9_margrel1(A) = k8_margrel1 )
        & ( A != k7_margrel1
         => k9_margrel1(A) = k7_margrel1 ) ) ) ),
    file(margrel1,d16_margrel1),
    [interesting(0.00)]).

fof(t7_armstrng,theorem,(
    $true ),
    file(armstrng,t7_armstrng),
    [interesting(0.00)]).