% Mizar problem: t34_relat_2,relat_2,466,40 
fof(t34_relat_2,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_relat_2(A)
       => v3_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_bg_added,[status(thm)],[involutiveness_k4_relat_1,dt_k4_relat_1,t30_relat_2]),
    [file(relat_2,t34_relat_2)]).

fof(involutiveness_k4_relat_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => k4_relat_1(k4_relat_1(A)) = A ) ),
    file(relat_1,k4_relat_1),
    []).

fof(dt_k4_relat_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => v1_relat_1(k4_relat_1(A)) ) ),
    file(relat_1,k4_relat_1),
    []).

fof(t30_relat_2,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_relat_2(A)
      <=> A = k4_relat_1(A) ) ) ),
    file(relat_2,t30_relat_2),
    []).