% Mizar problem: t8_amistd_3,amistd_3,236,69 
fof(t8_amistd_3,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( ( r4_wellord1(A,B)
              & v2_wellord1(A) )
           => v2_wellord1(B) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc1_amistd_1,d8_wellord1,t54_wellord1]),
    [file(amistd_3,t8_amistd_3)]).

fof(cc1_amistd_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_relat_1(A)
        & v1_setfam_1(A) ) ) ),
    file(amistd_1,cc1_amistd_1),
    []).

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(t54_wellord1,axiom,(
    ! [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) ) ) ) ) ),
    file(wellord1,t54_wellord1),
    []).