% Mizar problem: t54_wellord1,wellord1,997,20 
fof(t54_wellord1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C) )
             => ( ( v2_wellord1(A)
                  & r3_wellord1(A,B,C) )
               => v2_wellord1(B) ) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d4_wellord1,rc1_funct_1,t53_wellord1]),
    [file(wellord1,t54_wellord1)]).

fof(d4_wellord1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_wellord1(A)
      <=> ( v1_relat_2(A)
          & v8_relat_2(A)
          & v4_relat_2(A)
          & v6_relat_2(A)
          & v1_wellord1(A) ) ) ) ),
    file(wellord1,d4_wellord1),
    []).

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

fof(t53_wellord1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C) )
             => ( r3_wellord1(A,B,C)
               => ( ( v1_relat_2(A)
                   => v1_relat_2(B) )
                  & ( v8_relat_2(A)
                   => v8_relat_2(B) )
                  & ( v6_relat_2(A)
                   => v6_relat_2(B) )
                  & ( v4_relat_2(A)
                   => v4_relat_2(B) )
                  & ( v1_wellord1(A)
                   => v1_wellord1(B) ) ) ) ) ) ) ),
    file(wellord1,t53_wellord1),
    []).