% Mizar problem: t7_wellord2,wellord2,160,32 
fof(t7_wellord2,conjecture,(
    ! [A] : 
      ( v3_ordinal1(A)
     => v2_wellord1(k1_wellord2(A)) ) ),
    inference(mizar_bg_added,[status(thm)],[cc1_ordinal1,cc2_ordinal1,d4_wellord1,dt_k1_wellord2,rc1_ordinal1,t2_wellord2,t3_wellord2,t4_wellord2,t5_wellord2,t6_wellord2]),
    [file(wellord2,t7_wellord2)]).

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

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

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(dt_k1_wellord2,axiom,(
    ! [A] : v1_relat_1(k1_wellord2(A)) ),
    file(wellord2,k1_wellord2),
    []).

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

fof(t2_wellord2,axiom,(
    ! [A] : v1_relat_2(k1_wellord2(A)) ),
    file(wellord2,t2_wellord2),
    []).

fof(t3_wellord2,axiom,(
    ! [A] : v8_relat_2(k1_wellord2(A)) ),
    file(wellord2,t3_wellord2),
    []).

fof(t4_wellord2,axiom,(
    ! [A] : 
      ( v3_ordinal1(A)
     => v6_relat_2(k1_wellord2(A)) ) ),
    file(wellord2,t4_wellord2),
    []).

fof(t5_wellord2,axiom,(
    ! [A] : v4_relat_2(k1_wellord2(A)) ),
    file(wellord2,t5_wellord2),
    []).

fof(t6_wellord2,axiom,(
    ! [A] : 
      ( v3_ordinal1(A)
     => v1_wellord1(k1_wellord2(A)) ) ),
    file(wellord2,t6_wellord2),
    []).