% Mizar problem: t107_orders_1,orders_1,432,61 
fof(t107_orders_1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_wellord1(A)
       => ( v1_orders_1(A)
          & v2_orders_1(A)
          & v3_orders_1(A) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d3_orders_1,d4_orders_1,d4_wellord1,d5_orders_1]),
    [file(orders_1,t107_orders_1)]).

fof(d3_orders_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_orders_1(A)
      <=> ( v1_relat_2(A)
          & v8_relat_2(A) ) ) ) ),
    file(orders_1,d3_orders_1),
    []).

fof(d4_orders_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_orders_1(A)
      <=> ( v1_relat_2(A)
          & v8_relat_2(A)
          & v4_relat_2(A) ) ) ) ),
    file(orders_1,d4_orders_1),
    []).

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(d5_orders_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_orders_1(A)
      <=> ( v1_relat_2(A)
          & v8_relat_2(A)
          & v4_relat_2(A)
          & v6_relat_2(A) ) ) ) ),
    file(orders_1,d5_orders_1),
    []).