% Mizar problem: t24_zfmisc_1,zfmisc_1,385,25 
fof(t24_zfmisc_1,conjecture,(
    ! [A,B] : 
      ( r1_tarski(k1_tarski(A),k1_tarski(B))
     => A = B ) ),
    inference(mizar_bg_added,[status(thm)],[reflexivity_r1_tarski,dt_k1_tarski,t6_zfmisc_1]),
    [file(zfmisc_1,t24_zfmisc_1)]).

fof(reflexivity_r1_tarski,axiom,(
    ! [A,B] : r1_tarski(A,A) ),
    file(tarski,r1_tarski),
    []).

fof(dt_k1_tarski,axiom,(
    $true ),
    file(tarski,k1_tarski),
    []).

fof(t6_zfmisc_1,axiom,(
    ! [A,B] : 
      ( r1_tarski(k1_tarski(A),k1_tarski(B))
     => A = B ) ),
    file(zfmisc_1,t6_zfmisc_1),
    []).