% Mizar problem: t31_convex1,convex1,1726,55 
fof(t31_convex1,conjecture,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B,C,D] : ~ ( v2_funct_1(A)
          & k2_relat_1(A) = k1_enumset1(B,C,D)
          & B != C
          & C != D
          & D != B
          & A != k11_finseq_1(B,C,D)
          & A != k11_finseq_1(B,D,C)
          & A != k11_finseq_1(C,B,D)
          & A != k11_finseq_1(C,D,B)
          & A != k11_finseq_1(D,B,C)
          & A != k11_finseq_1(D,C,B) ) ) ),
    inference(mizar_bg_added,[status(thm)],[dt_k11_finseq_1,dt_k1_enumset1,dt_k2_relat_1,l39_convex1]),
    [file(convex1,t31_convex1)]).

fof(dt_k11_finseq_1,axiom,(
    $true ),
    file(finseq_1,k11_finseq_1),
    []).

fof(dt_k1_enumset1,axiom,(
    $true ),
    file(enumset1,k1_enumset1),
    []).

fof(dt_k2_relat_1,axiom,(
    $true ),
    file(relat_1,k2_relat_1),
    []).

fof(l39_convex1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B,C,D] : ~ ( v2_funct_1(A)
          & k2_relat_1(A) = k1_enumset1(B,C,D)
          & B != C
          & C != D
          & D != B
          & A != k11_finseq_1(B,C,D)
          & A != k11_finseq_1(B,D,C)
          & A != k11_finseq_1(C,B,D)
          & A != k11_finseq_1(C,D,B)
          & A != k11_finseq_1(D,B,C)
          & A != k11_finseq_1(D,C,B) ) ) ),
    file(convex1,l39_convex1),
    []).