% Mizar problem: t131_zfmisc_1,zfmisc_1,1639,71 
fof(t131_zfmisc_1,conjecture,(
    ! [A,B,C,D] : 
      ( A != B
     => ( r1_xboole_0(k2_zfmisc_1(k1_tarski(A),C),k2_zfmisc_1(k1_tarski(B),D))
        & r1_xboole_0(k2_zfmisc_1(C,k1_tarski(A)),k2_zfmisc_1(D,k1_tarski(B))) ) ) ),
    inference(mizar_bg_added,[status(thm)],[dt_k1_tarski,dt_k2_zfmisc_1,symmetry_r1_xboole_0,t127_zfmisc_1,t17_zfmisc_1]),
    [file(zfmisc_1,t131_zfmisc_1)]).

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

fof(dt_k2_zfmisc_1,axiom,(
    $true ),
    file(zfmisc_1,k2_zfmisc_1),
    []).

fof(symmetry_r1_xboole_0,axiom,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
     => r1_xboole_0(B,A) ) ),
    file(xboole_0,r1_xboole_0),
    []).

fof(t127_zfmisc_1,axiom,(
    ! [A,B,C,D] : 
      ( ( r1_xboole_0(A,B)
        | r1_xboole_0(C,D) )
     => r1_xboole_0(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ),
    file(zfmisc_1,t127_zfmisc_1),
    []).

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