% Mizar problem: t14_int_2,int_2,211,57 
fof(t14_int_2,conjecture,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( ( r2_int_1(A,B)
             => r2_int_1(A,k4_xcmplx_0(B)) )
            & ( r2_int_1(A,k4_xcmplx_0(B))
             => r2_int_1(A,B) )
            & ( r2_int_1(A,B)
             => r2_int_1(k4_xcmplx_0(A),B) )
            & ( r2_int_1(k4_xcmplx_0(A),B)
             => r2_int_1(A,B) )
            & ( r2_int_1(A,B)
             => r2_int_1(k4_xcmplx_0(A),k4_xcmplx_0(B)) )
            & ( r2_int_1(k4_xcmplx_0(A),k4_xcmplx_0(B))
             => r2_int_1(A,B) )
            & ( r2_int_1(A,k4_xcmplx_0(B))
             => r2_int_1(k4_xcmplx_0(A),B) )
            & ( r2_int_1(k4_xcmplx_0(A),B)
             => r2_int_1(A,k4_xcmplx_0(B)) ) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc4_int_1,dt_k4_xcmplx_0,fc3_int_1,involutiveness_k4_xcmplx_0,rc2_int_1,reflexivity_r2_int_1,t11_int_2,t13_int_2]),
    [file(int_2,t14_int_2)]).

fof(cc4_int_1,axiom,(
    ! [A] : 
      ( v1_int_1(A)
     => ( v1_xcmplx_0(A)
        & v1_xreal_0(A) ) ) ),
    file(int_1,cc4_int_1),
    []).

fof(dt_k4_xcmplx_0,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => v1_xcmplx_0(k4_xcmplx_0(A)) ) ),
    file(xcmplx_0,k4_xcmplx_0),
    []).

fof(fc3_int_1,axiom,(
    ! [A] : 
      ( v1_int_1(A)
     => ( v1_xcmplx_0(k4_xcmplx_0(A))
        & v1_xreal_0(k4_xcmplx_0(A))
        & v1_int_1(k4_xcmplx_0(A)) ) ) ),
    file(int_1,fc3_int_1),
    []).

fof(involutiveness_k4_xcmplx_0,axiom,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k4_xcmplx_0(k4_xcmplx_0(A)) = A ) ),
    file(xcmplx_0,k4_xcmplx_0),
    []).

fof(rc2_int_1,axiom,(
    ? [A] : v1_int_1(A) ),
    file(int_1,rc2_int_1),
    []).

fof(reflexivity_r2_int_1,axiom,(
    ! [A,B] : 
      ( ( v1_int_1(A)
        & v1_int_1(B) )
     => r2_int_1(A,A) ) ),
    file(int_1,r2_int_1),
    []).

fof(t11_int_2,axiom,(
    ! [A] : 
      ( v1_int_1(A)
     => ( r2_int_1(A,k4_xcmplx_0(A))
        & r2_int_1(k4_xcmplx_0(A),A) ) ) ),
    file(int_2,t11_int_2),
    []).

fof(t13_int_2,axiom,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( v1_int_1(C)
             => ( ( r2_int_1(A,B)
                  & r2_int_1(B,C) )
               => r2_int_1(A,C) ) ) ) ) ),
    file(int_2,t13_int_2),
    []).