% Mizar problem: t9_borsuk_5,borsuk_5,197,53 
fof(t9_borsuk_5,conjecture,(
    ! [A,B,C,D,E,F,G] : 
      ( r2_borsuk_5(A,B,C,D,E,F,G)
     => r2_borsuk_5(G,A,B,C,D,E,F) ) ),
    inference(mizar_bg_added,[status(thm)],[d2_borsuk_5]),
    [file(borsuk_5,t9_borsuk_5)]).

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