% Mizar problem: t108_orders_1,orders_1,441,70 
fof(t108_orders_1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_orders_1(A)
       => ( v1_orders_1(A)
          & v2_orders_1(A) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d3_orders_1,d4_orders_1,d5_orders_1]),
    [file(orders_1,t108_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(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),
    []).