% Mizar problem: t52_wellord1,wellord1,900,73 
fof(t52_wellord1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ! [C] : 
              ( v1_relat_1(C)
             => ( ( r4_wellord1(A,B)
                  & r4_wellord1(B,C) )
               => r4_wellord1(A,C) ) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d8_wellord1,dt_k5_relat_1,fc1_funct_1,rc1_funct_1,t51_wellord1]),
    [file(wellord1,t52_wellord1)]).

fof(d8_wellord1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( r4_wellord1(A,B)
          <=> ? [C] : 
                ( v1_relat_1(C)
                & v1_funct_1(C)
                & r3_wellord1(A,B,C) ) ) ) ) ),
    file(wellord1,d8_wellord1),
    []).

fof(dt_k5_relat_1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_relat_1(B) )
     => v1_relat_1(k5_relat_1(A,B)) ) ),
    file(relat_1,k5_relat_1),
    []).

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

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

fof(t51_wellord1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ! [C] : 
              ( v1_relat_1(C)
             => ! [D] : 
                  ( ( v1_relat_1(D)
                    & v1_funct_1(D) )
                 => ! [E] : 
                      ( ( v1_relat_1(E)
                        & v1_funct_1(E) )
                     => ( ( r3_wellord1(A,B,D)
                          & r3_wellord1(B,C,E) )
                       => r3_wellord1(A,C,k5_relat_1(D,E)) ) ) ) ) ) ) ),
    file(wellord1,t51_wellord1),
    []).