% Mizar problem: t7_borsuk_5,borsuk_5,163,51 
fof(t7_borsuk_5,conjecture,(
    ! [A,B,C,D,E,F] : 
      ( ( r1_incproj(A,B,C)
        & r1_incproj(D,E,F)
        & r1_xboole_0(k1_enumset1(A,B,C),k1_enumset1(D,E,F)) )
     => r1_borsuk_5(A,B,C,D,E,F) ) ),
    inference(mizar_bg_added,[status(thm)],[d1_borsuk_5,d5_incproj,dt_k1_enumset1,fc3_finset_1,symmetry_r1_xboole_0,t6_borsuk_5]),
    [file(borsuk_5,t7_borsuk_5)]).

fof(d1_borsuk_5,axiom,(
    ! [A,B,C,D,E,F] : 
      ( r1_borsuk_5(A,B,C,D,E,F)
    <=> ( A != B
        & A != C
        & A != D
        & A != E
        & A != F
        & B != C
        & B != D
        & B != E
        & B != F
        & C != D
        & C != E
        & C != F
        & D != E
        & D != F
        & E != F ) ) ),
    file(borsuk_5,d1_borsuk_5),
    []).

fof(d5_incproj,axiom,(
    ! [A,B,C] : 
      ( r1_incproj(A,B,C)
    <=> ( A != B
        & B != C
        & C != A ) ) ),
    file(incproj,d5_incproj),
    []).

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

fof(fc3_finset_1,axiom,(
    ! [A,B,C] : v1_finset_1(k1_enumset1(A,B,C)) ),
    file(finset_1,fc3_finset_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(t6_borsuk_5,axiom,(
    ! [A,B,C,D,E,F] : 
      ( r1_xboole_0(k1_enumset1(A,B,C),k1_enumset1(D,E,F))
     => ( A != D
        & A != E
        & A != F
        & B != D
        & B != E
        & B != F
        & C != D
        & C != E
        & C != F ) ) ),
    file(borsuk_5,t6_borsuk_5),
    []).