% Mizar problem: t9_zf_colla,zf_colla,386,47 
fof(t9_zf_colla,conjecture,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ? [B] : 
          ( v1_relat_1(B)
          & v1_funct_1(B)
          & k1_relat_1(B) = A
          & ! [C] : 
              ( m1_subset_1(C,A)
             => k1_funct_1(B,C) = k9_relat_1(B,C) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,cc10_membered,cc11_membered,cc12_membered,cc13_membered,cc14_membered,cc15_membered,cc16_membered,cc17_membered,cc18_membered,cc19_membered,cc1_funct_1,cc1_membered,cc1_ordinal1,cc20_membered,cc2_funct_1,cc2_membered,cc2_ordinal1,cc3_membered,cc3_ordinal1,cc4_membered,connectedness_r1_ordinal1,d10_xboole_0,d12_funct_1,d2_ordinal1,d3_tarski,dt_k1_funct_1,dt_k1_relat_1,dt_k1_xboole_0,dt_k1_zf_colla,dt_k1_zfmisc_1,dt_k7_relat_1,dt_k9_relat_1,dt_m1_subset_1,existence_m1_subset_1,fc2_ordinal1,fc4_funct_1,fc6_membered,rc1_funct_1,rc1_membered,rc1_ordinal1,rc2_funct_1,rc2_ordinal1,rc3_funct_1,rc3_ordinal1,rc4_funct_1,redefinition_r1_ordinal1,reflexivity_r1_ordinal1,reflexivity_r1_tarski,s1_tarski__e5_10_3_1__zf_colla,s2_funct_1__e4_10_3__zf_colla,s2_ordinal1__e3_10__zf_colla,s2_ordinal1__e5_10__zf_colla,s2_ordinal1__e7_10_3__zf_colla,t161_relat_1,t1_subset,t1_xboole_1,t22_ordinal1,t2_subset,t3_subset,t4_subset,t4_zf_colla,t5_subset,t6_boole,t6_zf_colla,t72_funct_1,t7_boole,t7_zf_colla,t82_funct_1,t8_boole,t8_zf_colla,t91_relat_1,t97_relat_1,t9_funct_1]),
    [file(zf_colla,t9_zf_colla)]).

fof(antisymmetry_r2_hidden,axiom,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => ~ r2_hidden(B,A) ) ),
    file(hidden,r2_hidden),
    []).

fof(cc10_membered,axiom,(
    ! [A] : 
      ( v1_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => v1_xcmplx_0(B) ) ) ),
    file(membered,cc10_membered),
    []).

fof(cc11_membered,axiom,(
    ! [A] : 
      ( v2_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ( v1_xcmplx_0(B)
            & v1_xreal_0(B) ) ) ) ),
    file(membered,cc11_membered),
    []).

fof(cc12_membered,axiom,(
    ! [A] : 
      ( v3_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ( v1_xcmplx_0(B)
            & v1_xreal_0(B)
            & v1_rat_1(B) ) ) ) ),
    file(membered,cc12_membered),
    []).

fof(cc13_membered,axiom,(
    ! [A] : 
      ( v4_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ( v1_xcmplx_0(B)
            & v1_xreal_0(B)
            & v1_int_1(B)
            & v1_rat_1(B) ) ) ) ),
    file(membered,cc13_membered),
    []).

fof(cc14_membered,axiom,(
    ! [A] : 
      ( v5_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ( v1_xcmplx_0(B)
            & v4_ordinal2(B)
            & v1_xreal_0(B)
            & v1_int_1(B)
            & v1_rat_1(B) ) ) ) ),
    file(membered,cc14_membered),
    []).

fof(cc15_membered,axiom,(
    ! [A] : 
      ( v1_xboole_0(A)
     => ( v1_membered(A)
        & v2_membered(A)
        & v3_membered(A)
        & v4_membered(A)
        & v5_membered(A) ) ) ),
    file(membered,cc15_membered),
    []).

fof(cc16_membered,axiom,(
    ! [A] : 
      ( v1_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => v1_membered(B) ) ) ),
    file(membered,cc16_membered),
    []).

fof(cc17_membered,axiom,(
    ! [A] : 
      ( v2_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ( v1_membered(B)
            & v2_membered(B) ) ) ) ),
    file(membered,cc17_membered),
    []).

fof(cc18_membered,axiom,(
    ! [A] : 
      ( v3_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ( v1_membered(B)
            & v2_membered(B)
            & v3_membered(B) ) ) ) ),
    file(membered,cc18_membered),
    []).

fof(cc19_membered,axiom,(
    ! [A] : 
      ( v4_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ( v1_membered(B)
            & v2_membered(B)
            & v3_membered(B)
            & v4_membered(B) ) ) ) ),
    file(membered,cc19_membered),
    []).

fof(cc1_funct_1,axiom,(
    ! [A] : 
      ( v1_xboole_0(A)
     => v1_funct_1(A) ) ),
    file(funct_1,cc1_funct_1),
    []).

fof(cc1_membered,axiom,(
    ! [A] : 
      ( v5_membered(A)
     => v4_membered(A) ) ),
    file(membered,cc1_membered),
    []).

fof(cc1_ordinal1,axiom,(
    ! [A] : 
      ( v3_ordinal1(A)
     => ( v1_ordinal1(A)
        & v2_ordinal1(A) ) ) ),
    file(ordinal1,cc1_ordinal1),
    []).

fof(cc20_membered,axiom,(
    ! [A] : 
      ( v5_membered(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ( v1_membered(B)
            & v2_membered(B)
            & v3_membered(B)
            & v4_membered(B)
            & v5_membered(B) ) ) ) ),
    file(membered,cc20_membered),
    []).

fof(cc2_funct_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_xboole_0(A)
        & v1_funct_1(A) )
     => ( v1_relat_1(A)
        & v1_funct_1(A)
        & v2_funct_1(A) ) ) ),
    file(funct_1,cc2_funct_1),
    []).

fof(cc2_membered,axiom,(
    ! [A] : 
      ( v4_membered(A)
     => v3_membered(A) ) ),
    file(membered,cc2_membered),
    []).

fof(cc2_ordinal1,axiom,(
    ! [A] : 
      ( ( v1_ordinal1(A)
        & v2_ordinal1(A) )
     => v3_ordinal1(A) ) ),
    file(ordinal1,cc2_ordinal1),
    []).

fof(cc3_membered,axiom,(
    ! [A] : 
      ( v3_membered(A)
     => v2_membered(A) ) ),
    file(membered,cc3_membered),
    []).

fof(cc3_ordinal1,axiom,(
    ! [A] : 
      ( v1_xboole_0(A)
     => ( v1_ordinal1(A)
        & v2_ordinal1(A)
        & v3_ordinal1(A) ) ) ),
    file(ordinal1,cc3_ordinal1),
    []).

fof(cc4_membered,axiom,(
    ! [A] : 
      ( v2_membered(A)
     => v1_membered(A) ) ),
    file(membered,cc4_membered),
    []).

fof(connectedness_r1_ordinal1,axiom,(
    ! [A,B] : 
      ( ( v3_ordinal1(A)
        & v3_ordinal1(B) )
     => ( r1_ordinal1(A,B)
        | r1_ordinal1(B,A) ) ) ),
    file(ordinal1,r1_ordinal1),
    []).

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

fof(d12_funct_1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( C = k9_relat_1(A,B)
        <=> ! [D] : 
              ( r2_hidden(D,C)
            <=> ? [E] : 
                  ( r2_hidden(E,k1_relat_1(A))
                  & r2_hidden(E,B)
                  & D = k1_funct_1(A,E) ) ) ) ) ),
    file(funct_1,d12_funct_1),
    []).

fof(d2_ordinal1,axiom,(
    ! [A] : 
      ( v1_ordinal1(A)
    <=> ! [B] : 
          ( r2_hidden(B,A)
         => r1_tarski(B,A) ) ) ),
    file(ordinal1,d2_ordinal1),
    []).

fof(d3_tarski,axiom,(
    ! [A,B] : 
      ( r1_tarski(A,B)
    <=> ! [C] : 
          ( r2_hidden(C,A)
         => r2_hidden(C,B) ) ) ),
    file(tarski,d3_tarski),
    []).

fof(dt_k1_funct_1,axiom,(
    $true ),
    file(funct_1,k1_funct_1),
    []).

fof(dt_k1_relat_1,axiom,(
    $true ),
    file(relat_1,k1_relat_1),
    []).

fof(dt_k1_xboole_0,axiom,(
    $true ),
    file(xboole_0,k1_xboole_0),
    []).

fof(dt_k1_zf_colla,axiom,(
    $true ),
    file(zf_colla,k1_zf_colla),
    []).

fof(dt_k1_zfmisc_1,axiom,(
    $true ),
    file(zfmisc_1,k1_zfmisc_1),
    []).

fof(dt_k7_relat_1,axiom,(
    ! [A,B] : 
      ( v1_relat_1(A)
     => v1_relat_1(k7_relat_1(A,B)) ) ),
    file(relat_1,k7_relat_1),
    []).

fof(dt_k9_relat_1,axiom,(
    $true ),
    file(relat_1,k9_relat_1),
    []).

fof(dt_m1_subset_1,axiom,(
    $true ),
    file(subset_1,m1_subset_1),
    []).

fof(existence_m1_subset_1,axiom,(
    ! [A] : 
    ? [B] : m1_subset_1(B,A) ),
    file(subset_1,m1_subset_1),
    []).

fof(fc2_ordinal1,axiom,
    ( v1_relat_1(k1_xboole_0)
    & v3_relat_1(k1_xboole_0)
    & v1_funct_1(k1_xboole_0)
    & v2_funct_1(k1_xboole_0)
    & v1_xboole_0(k1_xboole_0)
    & v1_ordinal1(k1_xboole_0)
    & v2_ordinal1(k1_xboole_0)
    & v3_ordinal1(k1_xboole_0) ),
    file(ordinal1,fc2_ordinal1),
    []).

fof(fc4_funct_1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_relat_1(k7_relat_1(A,B))
        & v1_funct_1(k7_relat_1(A,B)) ) ) ),
    file(funct_1,fc4_funct_1),
    []).

fof(fc6_membered,axiom,
    ( v1_xboole_0(k1_xboole_0)
    & v1_membered(k1_xboole_0)
    & v2_membered(k1_xboole_0)
    & v3_membered(k1_xboole_0)
    & v4_membered(k1_xboole_0)
    & v5_membered(k1_xboole_0) ),
    file(membered,fc6_membered),
    []).

fof(rc1_funct_1,axiom,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A) ) ),
    file(funct_1,rc1_funct_1),
    []).

fof(rc1_membered,axiom,(
    ? [A] : 
      ( ~ v1_xboole_0(A)
      & v1_membered(A)
      & v2_membered(A)
      & v3_membered(A)
      & v4_membered(A)
      & v5_membered(A) ) ),
    file(membered,rc1_membered),
    []).

fof(rc1_ordinal1,axiom,(
    ? [A] : 
      ( v1_ordinal1(A)
      & v2_ordinal1(A)
      & v3_ordinal1(A) ) ),
    file(ordinal1,rc1_ordinal1),
    []).

fof(rc2_funct_1,axiom,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_xboole_0(A)
      & v1_funct_1(A) ) ),
    file(funct_1,rc2_funct_1),
    []).

fof(rc2_ordinal1,axiom,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A)
      & v2_funct_1(A)
      & v1_xboole_0(A)
      & v1_ordinal1(A)
      & v2_ordinal1(A)
      & v3_ordinal1(A) ) ),
    file(ordinal1,rc2_ordinal1),
    []).

fof(rc3_funct_1,axiom,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A)
      & v2_funct_1(A) ) ),
    file(funct_1,rc3_funct_1),
    []).

fof(rc3_ordinal1,axiom,(
    ? [A] : 
      ( ~ v1_xboole_0(A)
      & v1_ordinal1(A)
      & v2_ordinal1(A)
      & v3_ordinal1(A) ) ),
    file(ordinal1,rc3_ordinal1),
    []).

fof(rc4_funct_1,axiom,(
    ? [A] : 
      ( v1_relat_1(A)
      & v3_relat_1(A)
      & v1_funct_1(A) ) ),
    file(funct_1,rc4_funct_1),
    []).

fof(redefinition_r1_ordinal1,axiom,(
    ! [A,B] : 
      ( ( v3_ordinal1(A)
        & v3_ordinal1(B) )
     => ( r1_ordinal1(A,B)
      <=> r1_tarski(A,B) ) ) ),
    file(ordinal1,r1_ordinal1),
    []).

fof(reflexivity_r1_ordinal1,axiom,(
    ! [A,B] : 
      ( ( v3_ordinal1(A)
        & v3_ordinal1(B) )
     => r1_ordinal1(A,A) ) ),
    file(ordinal1,r1_ordinal1),
    []).

fof(reflexivity_r1_tarski,axiom,(
    ! [A,B] : r1_tarski(A,A) ),
    file(tarski,r1_tarski),
    []).

fof(s1_tarski__e5_10_3_1__zf_colla,axiom,(
    ! [A,B,C] : 
      ( ( ~ v1_xboole_0(A)
        & v3_ordinal1(B)
        & m1_subset_1(C,A) )
     => ( ! [D,E,F] : 
            ( ( ? [G] : 
                  ( v3_ordinal1(G)
                  & ? [H] : 
                      ( v1_relat_1(H)
                      & v1_funct_1(H)
                      & r2_hidden(G,B)
                      & r2_hidden(D,k1_zf_colla(A,G))
                      & k1_relat_1(H) = k1_zf_colla(A,G)
                      & ! [I] : 
                          ( m1_subset_1(I,A)
                         => ( r2_hidden(I,k1_zf_colla(A,G))
                           => k1_funct_1(H,I) = k9_relat_1(H,I) ) )
                      & E = k1_funct_1(H,D) ) )
              & ? [J] : 
                  ( v3_ordinal1(J)
                  & ? [K] : 
                      ( v1_relat_1(K)
                      & v1_funct_1(K)
                      & r2_hidden(J,B)
                      & r2_hidden(D,k1_zf_colla(A,J))
                      & k1_relat_1(K) = k1_zf_colla(A,J)
                      & ! [L] : 
                          ( m1_subset_1(L,A)
                         => ( r2_hidden(L,k1_zf_colla(A,J))
                           => k1_funct_1(K,L) = k9_relat_1(K,L) ) )
                      & F = k1_funct_1(K,D) ) ) )
           => E = F )
       => ? [D] : 
          ! [E] : 
            ( r2_hidden(E,D)
          <=> ? [F] : 
                ( r2_hidden(F,C)
                & ? [M] : 
                    ( v3_ordinal1(M)
                    & ? [N] : 
                        ( v1_relat_1(N)
                        & v1_funct_1(N)
                        & r2_hidden(M,B)
                        & r2_hidden(F,k1_zf_colla(A,M))
                        & k1_relat_1(N) = k1_zf_colla(A,M)
                        & ! [O] : 
                            ( m1_subset_1(O,A)
                           => ( r2_hidden(O,k1_zf_colla(A,M))
                             => k1_funct_1(N,O) = k9_relat_1(N,O) ) )
                        & E = k1_funct_1(N,F) ) ) ) ) ) ) ),
    file(zf_colla,s1_tarski__e5_10_3_1__zf_colla),
    []).

fof(s2_funct_1__e4_10_3__zf_colla,axiom,(
    ! [A,B] : 
      ( ( ~ v1_xboole_0(A)
        & v3_ordinal1(B) )
     => ( ( ! [C,D,E] : 
              ( ( r2_hidden(C,k1_zf_colla(A,B))
                & ? [F,G] : 
                    ( m1_subset_1(G,A)
                    & F = D
                    & G = C
                    & ! [H] : 
                        ( r2_hidden(H,F)
                      <=> ? [I] : 
                            ( m1_subset_1(I,A)
                            & ? [J] : 
                                ( v3_ordinal1(J)
                                & ? [K] : 
                                    ( v1_relat_1(K)
                                    & v1_funct_1(K)
                                    & r2_hidden(I,G)
                                    & r2_hidden(J,B)
                                    & r2_hidden(I,k1_zf_colla(A,J))
                                    & k1_relat_1(K) = k1_zf_colla(A,J)
                                    & ! [L] : 
                                        ( m1_subset_1(L,A)
                                       => ( r2_hidden(L,k1_zf_colla(A,J))
                                         => k1_funct_1(K,L) = k9_relat_1(K,L) ) )
                                    & H = k1_funct_1(K,I) ) ) ) ) )
                & ? [M,N] : 
                    ( m1_subset_1(N,A)
                    & M = E
                    & N = C
                    & ! [O] : 
                        ( r2_hidden(O,M)
                      <=> ? [P] : 
                            ( m1_subset_1(P,A)
                            & ? [Q] : 
                                ( v3_ordinal1(Q)
                                & ? [R] : 
                                    ( v1_relat_1(R)
                                    & v1_funct_1(R)
                                    & r2_hidden(P,N)
                                    & r2_hidden(Q,B)
                                    & r2_hidden(P,k1_zf_colla(A,Q))
                                    & k1_relat_1(R) = k1_zf_colla(A,Q)
                                    & ! [S] : 
                                        ( m1_subset_1(S,A)
                                       => ( r2_hidden(S,k1_zf_colla(A,Q))
                                         => k1_funct_1(R,S) = k9_relat_1(R,S) ) )
                                    & O = k1_funct_1(R,P) ) ) ) ) ) )
             => D = E )
          & ! [C] : ~ ( r2_hidden(C,k1_zf_colla(A,B))
              & ! [D] : ~ ? [T,U] : 
                    ( m1_subset_1(U,A)
                    & T = D
                    & U = C
                    & ! [V] : 
                        ( r2_hidden(V,T)
                      <=> ? [W] : 
                            ( m1_subset_1(W,A)
                            & ? [X] : 
                                ( v3_ordinal1(X)
                                & ? [Y] : 
                                    ( v1_relat_1(Y)
                                    & v1_funct_1(Y)
                                    & r2_hidden(W,U)
                                    & r2_hidden(X,B)
                                    & r2_hidden(W,k1_zf_colla(A,X))
                                    & k1_relat_1(Y) = k1_zf_colla(A,X)
                                    & ! [Z] : 
                                        ( m1_subset_1(Z,A)
                                       => ( r2_hidden(Z,k1_zf_colla(A,X))
                                         => k1_funct_1(Y,Z) = k9_relat_1(Y,Z) ) )
                                    & V = k1_funct_1(Y,W) ) ) ) ) ) ) )
       => ? [C] : 
            ( v1_relat_1(C)
            & v1_funct_1(C)
            & k1_relat_1(C) = k1_zf_colla(A,B)
            & ! [D] : 
                ( r2_hidden(D,k1_zf_colla(A,B))
               => ? [A1,B1] : 
                    ( m1_subset_1(B1,A)
                    & A1 = k1_funct_1(C,D)
                    & B1 = D
                    & ! [C1] : 
                        ( r2_hidden(C1,A1)
                      <=> ? [D1] : 
                            ( m1_subset_1(D1,A)
                            & ? [E1] : 
                                ( v3_ordinal1(E1)
                                & ? [F1] : 
                                    ( v1_relat_1(F1)
                                    & v1_funct_1(F1)
                                    & r2_hidden(D1,B1)
                                    & r2_hidden(E1,B)
                                    & r2_hidden(D1,k1_zf_colla(A,E1))
                                    & k1_relat_1(F1) = k1_zf_colla(A,E1)
                                    & ! [G1] : 
                                        ( m1_subset_1(G1,A)
                                       => ( r2_hidden(G1,k1_zf_colla(A,E1))
                                         => k1_funct_1(F1,G1) = k9_relat_1(F1,G1) ) )
                                    & C1 = k1_funct_1(F1,D1) ) ) ) ) ) ) ) ) ) ),
    file(zf_colla,s2_funct_1__e4_10_3__zf_colla),
    []).

fof(s2_ordinal1__e3_10__zf_colla,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( v3_ordinal1(B)
           => ( ! [C] : 
                  ( v3_ordinal1(C)
                 => ( r2_hidden(C,B)
                   => ! [D] : 
                        ( ( v1_relat_1(D)
                          & v1_funct_1(D) )
                       => ! [E] : 
                            ( ( v1_relat_1(E)
                              & v1_funct_1(E) )
                           => ( ( k1_relat_1(D) = k1_zf_colla(A,C)
                                & ! [F] : 
                                    ( m1_subset_1(F,A)
                                   => ( r2_hidden(F,k1_zf_colla(A,C))
                                     => k1_funct_1(D,F) = k9_relat_1(D,F) ) )
                                & k1_relat_1(E) = k1_zf_colla(A,C)
                                & ! [F] : 
                                    ( m1_subset_1(F,A)
                                   => ( r2_hidden(F,k1_zf_colla(A,C))
                                     => k1_funct_1(E,F) = k9_relat_1(E,F) ) ) )
                             => D = E ) ) ) ) )
             => ! [G] : 
                  ( ( v1_relat_1(G)
                    & v1_funct_1(G) )
                 => ! [H] : 
                      ( ( v1_relat_1(H)
                        & v1_funct_1(H) )
                     => ( ( k1_relat_1(G) = k1_zf_colla(A,B)
                          & ! [I] : 
                              ( m1_subset_1(I,A)
                             => ( r2_hidden(I,k1_zf_colla(A,B))
                               => k1_funct_1(G,I) = k9_relat_1(G,I) ) )
                          & k1_relat_1(H) = k1_zf_colla(A,B)
                          & ! [I] : 
                              ( m1_subset_1(I,A)
                             => ( r2_hidden(I,k1_zf_colla(A,B))
                               => k1_funct_1(H,I) = k9_relat_1(H,I) ) ) )
                       => G = H ) ) ) ) )
       => ! [B] : 
            ( v3_ordinal1(B)
           => ! [J] : 
                ( ( v1_relat_1(J)
                  & v1_funct_1(J) )
               => ! [K] : 
                    ( ( v1_relat_1(K)
                      & v1_funct_1(K) )
                   => ( ( k1_relat_1(J) = k1_zf_colla(A,B)
                        & ! [L] : 
                            ( m1_subset_1(L,A)
                           => ( r2_hidden(L,k1_zf_colla(A,B))
                             => k1_funct_1(J,L) = k9_relat_1(J,L) ) )
                        & k1_relat_1(K) = k1_zf_colla(A,B)
                        & ! [L] : 
                            ( m1_subset_1(L,A)
                           => ( r2_hidden(L,k1_zf_colla(A,B))
                             => k1_funct_1(K,L) = k9_relat_1(K,L) ) ) )
                     => J = K ) ) ) ) ) ) ),
    file(zf_colla,s2_ordinal1__e3_10__zf_colla),
    []).

fof(s2_ordinal1__e5_10__zf_colla,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( v3_ordinal1(B)
           => ( ! [C] : 
                  ( v3_ordinal1(C)
                 => ( r2_hidden(C,B)
                   => ? [D] : 
                        ( v1_relat_1(D)
                        & v1_funct_1(D)
                        & k1_relat_1(D) = k1_zf_colla(A,C)
                        & ! [E] : 
                            ( m1_subset_1(E,A)
                           => ( r2_hidden(E,k1_zf_colla(A,C))
                             => k1_funct_1(D,E) = k9_relat_1(D,E) ) ) ) ) )
             => ? [F] : 
                  ( v1_relat_1(F)
                  & v1_funct_1(F)
                  & k1_relat_1(F) = k1_zf_colla(A,B)
                  & ! [G] : 
                      ( m1_subset_1(G,A)
                     => ( r2_hidden(G,k1_zf_colla(A,B))
                       => k1_funct_1(F,G) = k9_relat_1(F,G) ) ) ) ) )
       => ! [B] : 
            ( v3_ordinal1(B)
           => ? [H] : 
                ( v1_relat_1(H)
                & v1_funct_1(H)
                & k1_relat_1(H) = k1_zf_colla(A,B)
                & ! [I] : 
                    ( m1_subset_1(I,A)
                   => ( r2_hidden(I,k1_zf_colla(A,B))
                     => k1_funct_1(H,I) = k9_relat_1(H,I) ) ) ) ) ) ) ),
    file(zf_colla,s2_ordinal1__e5_10__zf_colla),
    []).

fof(s2_ordinal1__e7_10_3__zf_colla,axiom,(
    ! [A,B,C] : 
      ( ( ~ v1_xboole_0(A)
        & v3_ordinal1(B)
        & v1_relat_1(C)
        & v1_funct_1(C) )
     => ( ! [D] : 
            ( v3_ordinal1(D)
           => ( ! [E] : 
                  ( v3_ordinal1(E)
                 => ( r2_hidden(E,D)
                   => ( r1_ordinal1(E,B)
                     => ( k1_relat_1(k7_relat_1(C,k1_zf_colla(A,E))) = k1_zf_colla(A,E)
                        & ! [F] : 
                            ( m1_subset_1(F,A)
                           => ( r2_hidden(F,k1_zf_colla(A,E))
                             => k1_funct_1(k7_relat_1(C,k1_zf_colla(A,E)),F) = k9_relat_1(k7_relat_1(C,k1_zf_colla(A,E)),F) ) ) ) ) ) )
             => ( r1_ordinal1(D,B)
               => ( k1_relat_1(k7_relat_1(C,k1_zf_colla(A,D))) = k1_zf_colla(A,D)
                  & ! [G] : 
                      ( m1_subset_1(G,A)
                     => ( r2_hidden(G,k1_zf_colla(A,D))
                       => k1_funct_1(k7_relat_1(C,k1_zf_colla(A,D)),G) = k9_relat_1(k7_relat_1(C,k1_zf_colla(A,D)),G) ) ) ) ) ) )
       => ! [D] : 
            ( v3_ordinal1(D)
           => ( r1_ordinal1(D,B)
             => ( k1_relat_1(k7_relat_1(C,k1_zf_colla(A,D))) = k1_zf_colla(A,D)
                & ! [H] : 
                    ( m1_subset_1(H,A)
                   => ( r2_hidden(H,k1_zf_colla(A,D))
                     => k1_funct_1(k7_relat_1(C,k1_zf_colla(A,D)),H) = k9_relat_1(k7_relat_1(C,k1_zf_colla(A,D)),H) ) ) ) ) ) ) ) ),
    file(zf_colla,s2_ordinal1__e7_10_3__zf_colla),
    []).

fof(t161_relat_1,axiom,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => r1_tarski(k9_relat_1(k7_relat_1(C,A),B),k9_relat_1(C,B)) ) ),
    file(relat_1,t161_relat_1),
    []).

fof(t1_subset,axiom,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => m1_subset_1(A,B) ) ),
    file(subset,t1_subset),
    []).

fof(t1_xboole_1,axiom,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(B,C) )
     => r1_tarski(A,C) ) ),
    file(xboole_1,t1_xboole_1),
    []).

fof(t22_ordinal1,axiom,(
    ! [A] : 
      ( v1_ordinal1(A)
     => ! [B] : 
          ( v3_ordinal1(B)
         => ! [C] : 
              ( v3_ordinal1(C)
             => ( ( r1_tarski(A,B)
                  & r2_hidden(B,C) )
               => r2_hidden(A,C) ) ) ) ) ),
    file(ordinal1,t22_ordinal1),
    []).

fof(t2_subset,axiom,(
    ! [A,B] : 
      ( m1_subset_1(A,B)
     => ( v1_xboole_0(B)
        | r2_hidden(A,B) ) ) ),
    file(subset,t2_subset),
    []).

fof(t3_subset,axiom,(
    ! [A,B] : 
      ( m1_subset_1(A,k1_zfmisc_1(B))
    <=> r1_tarski(A,B) ) ),
    file(subset,t3_subset),
    []).

fof(t4_subset,axiom,(
    ! [A,B,C] : 
      ( ( r2_hidden(A,B)
        & m1_subset_1(B,k1_zfmisc_1(C)) )
     => m1_subset_1(A,C) ) ),
    file(subset,t4_subset),
    []).

fof(t4_zf_colla,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( v3_ordinal1(B)
         => ! [C] : 
              ( v3_ordinal1(C)
             => ( r1_ordinal1(B,C)
               => r1_tarski(k1_zf_colla(A,B),k1_zf_colla(A,C)) ) ) ) ) ),
    file(zf_colla,t4_zf_colla),
    []).

fof(t5_subset,axiom,(
    ! [A,B,C] : ~ ( r2_hidden(A,B)
      & m1_subset_1(B,k1_zfmisc_1(C))
      & v1_xboole_0(C) ) ),
    file(subset,t5_subset),
    []).

fof(t6_boole,axiom,(
    ! [A] : 
      ( v1_xboole_0(A)
     => A = k1_xboole_0 ) ),
    file(boole,t6_boole),
    []).

fof(t6_zf_colla,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( v3_ordinal1(B)
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ! [D] : 
                  ( m1_subset_1(D,A)
                 => ( ( r2_hidden(C,D)
                      & r2_hidden(D,k1_zf_colla(A,B)) )
                   => ( r2_hidden(C,k1_zf_colla(A,B))
                      & ? [E] : 
                          ( v3_ordinal1(E)
                          & r2_hidden(E,B)
                          & r2_hidden(C,k1_zf_colla(A,E)) ) ) ) ) ) ) ) ),
    file(zf_colla,t6_zf_colla),
    []).

fof(t72_funct_1,axiom,(
    ! [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),
    []).

fof(t7_boole,axiom,(
    ! [A,B] : ~ ( r2_hidden(A,B)
      & v1_xboole_0(B) ) ),
    file(boole,t7_boole),
    []).

fof(t7_zf_colla,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( v3_ordinal1(B)
         => r1_tarski(k1_zf_colla(A,B),A) ) ) ),
    file(zf_colla,t7_zf_colla),
    []).

fof(t82_funct_1,axiom,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r1_tarski(A,B)
       => ( k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,A)
          & k7_relat_1(k7_relat_1(C,B),A) = k7_relat_1(C,A) ) ) ) ),
    file(funct_1,t82_funct_1),
    []).

fof(t8_boole,axiom,(
    ! [A,B] : ~ ( v1_xboole_0(A)
      & A != B
      & v1_xboole_0(B) ) ),
    file(boole,t8_boole),
    []).

fof(t8_zf_colla,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ? [B] : 
          ( v3_ordinal1(B)
          & A = k1_zf_colla(A,B) ) ) ),
    file(zf_colla,t8_zf_colla),
    []).

fof(t91_relat_1,axiom,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(A,k1_relat_1(B))
       => k1_relat_1(k7_relat_1(B,A)) = A ) ) ),
    file(relat_1,t91_relat_1),
    []).

fof(t97_relat_1,axiom,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(k1_relat_1(B),A)
       => k7_relat_1(B,A) = B ) ) ),
    file(relat_1,t97_relat_1),
    []).

fof(t9_funct_1,axiom,(
    ! [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),
    []).