% Mizar problem: t109_orders_1,orders_1,449,45 
fof(t109_orders_1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_orders_1(A)
       => v1_orders_1(A) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d3_orders_1,d4_orders_1]),
    [file(orders_1,t109_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),
    []).