% Mizar problem: t1_graph_3,graph_3,54,72 
fof(t1_graph_3,conjecture,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( ( v1_abian(A)
            <=> v1_abian(B) )
          <=> v1_abian(k6_xcmplx_0(A,B)) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc2_xreal_0,cc4_int_1,dt_k6_xcmplx_0,fc13_abian,fc14_abian,fc15_abian,fc1_graph_3,fc4_int_1,fc5_xreal_0,rc1_xreal_0,rc2_int_1,rc3_abian,rc4_abian]),
    [file(graph_3,t1_graph_3)]).

fof(cc2_xreal_0,axiom,(
    ! [A] : 
      ( v1_xreal_0(A)
     => v1_xcmplx_0(A) ) ),
    file(xreal_0,cc2_xreal_0),
    []).

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_k6_xcmplx_0,axiom,(
    $true ),
    file(xcmplx_0,k6_xcmplx_0),
    []).

fof(fc13_abian,axiom,(
    ! [A,B] : 
      ( ( v1_int_1(A)
        & v1_abian(A)
        & v1_int_1(B)
        & ~ v1_abian(B) )
     => ( v1_xcmplx_0(k6_xcmplx_0(A,B))
        & v1_xreal_0(k6_xcmplx_0(A,B))
        & v1_int_1(k6_xcmplx_0(A,B))
        & ~ v1_abian(k6_xcmplx_0(A,B)) ) ) ),
    file(abian,fc13_abian),
    []).

fof(fc14_abian,axiom,(
    ! [A,B] : 
      ( ( v1_int_1(A)
        & v1_abian(A)
        & v1_int_1(B)
        & ~ v1_abian(B) )
     => ( v1_xcmplx_0(k6_xcmplx_0(B,A))
        & v1_xreal_0(k6_xcmplx_0(B,A))
        & v1_int_1(k6_xcmplx_0(B,A))
        & ~ v1_abian(k6_xcmplx_0(B,A)) ) ) ),
    file(abian,fc14_abian),
    []).

fof(fc15_abian,axiom,(
    ! [A,B] : 
      ( ( v1_int_1(A)
        & ~ v1_abian(A)
        & v1_int_1(B)
        & ~ v1_abian(B) )
     => ( v1_xcmplx_0(k6_xcmplx_0(A,B))
        & v1_xreal_0(k6_xcmplx_0(A,B))
        & v1_int_1(k6_xcmplx_0(A,B))
        & v1_abian(k6_xcmplx_0(A,B)) ) ) ),
    file(abian,fc15_abian),
    []).

fof(fc1_graph_3,axiom,(
    ! [A,B] : 
      ( ( v1_int_1(A)
        & v1_abian(A)
        & v1_int_1(B)
        & v1_abian(B) )
     => ( v1_xreal_0(k6_xcmplx_0(A,B))
        & v1_int_1(k6_xcmplx_0(A,B))
        & v1_xcmplx_0(k6_xcmplx_0(A,B))
        & v1_abian(k6_xcmplx_0(A,B)) ) ) ),
    file(graph_3,fc1_graph_3),
    []).

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

fof(fc5_xreal_0,axiom,(
    ! [A,B] : 
      ( ( v1_xreal_0(A)
        & v1_xreal_0(B) )
     => ( v1_xcmplx_0(k6_xcmplx_0(A,B))
        & v1_xreal_0(k6_xcmplx_0(A,B)) ) ) ),
    file(xreal_0,fc5_xreal_0),
    []).

fof(rc1_xreal_0,axiom,(
    ? [A] : 
      ( v1_xcmplx_0(A)
      & v1_xreal_0(A) ) ),
    file(xreal_0,rc1_xreal_0),
    []).

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

fof(rc3_abian,axiom,(
    ? [A] : 
      ( v1_xcmplx_0(A)
      & v1_xreal_0(A)
      & v1_int_1(A)
      & v1_abian(A) ) ),
    file(abian,rc3_abian),
    []).

fof(rc4_abian,axiom,(
    ? [A] : 
      ( v1_xcmplx_0(A)
      & v1_xreal_0(A)
      & v1_int_1(A)
      & ~ v1_abian(A) ) ),
    file(abian,rc4_abian),
    []).