let n be Nat; :: thesis: n -SuccRelStr is asymmetric

set S = n -SuccRelStr ;

the InternalRel of (n -SuccRelStr) is_asymmetric_in field the InternalRel of (n -SuccRelStr)

set S = n -SuccRelStr ;

the InternalRel of (n -SuccRelStr) is_asymmetric_in field the InternalRel of (n -SuccRelStr)

proof

hence
the InternalRel of (n -SuccRelStr) is asymmetric
; :: according to NECKLACE:def 4 :: thesis: verum
let x, y be object ; :: according to RELAT_2:def 5 :: thesis: ( not x in field the InternalRel of (n -SuccRelStr) or not y in field the InternalRel of (n -SuccRelStr) or not [x,y] in the InternalRel of (n -SuccRelStr) or not [y,x] in the InternalRel of (n -SuccRelStr) )

assume that

x in field the InternalRel of (n -SuccRelStr) and

y in field the InternalRel of (n -SuccRelStr) and

A1: [x,y] in the InternalRel of (n -SuccRelStr) ; :: thesis: not [y,x] in the InternalRel of (n -SuccRelStr)

A2: [x,y] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by A1, Def6;

assume [y,x] in the InternalRel of (n -SuccRelStr) ; :: thesis: contradiction

then [y,x] in { [i9,(i9 + 1)] where i9 is Element of NAT : i9 + 1 < n } by Def6;

then consider j being Element of NAT such that

A3: [y,x] = [j,(j + 1)] and

j + 1 < n ;

A4: ( y = j & x = j + 1 ) by A3, XTUPLE_0:1;

consider i being Element of NAT such that

A5: [x,y] = [i,(i + 1)] and

i + 1 < n by A2;

( x = i & y = i + 1 ) by A5, XTUPLE_0:1;

hence contradiction by A4; :: thesis: verum

end;assume that

x in field the InternalRel of (n -SuccRelStr) and

y in field the InternalRel of (n -SuccRelStr) and

A1: [x,y] in the InternalRel of (n -SuccRelStr) ; :: thesis: not [y,x] in the InternalRel of (n -SuccRelStr)

A2: [x,y] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by A1, Def6;

assume [y,x] in the InternalRel of (n -SuccRelStr) ; :: thesis: contradiction

then [y,x] in { [i9,(i9 + 1)] where i9 is Element of NAT : i9 + 1 < n } by Def6;

then consider j being Element of NAT such that

A3: [y,x] = [j,(j + 1)] and

j + 1 < n ;

A4: ( y = j & x = j + 1 ) by A3, XTUPLE_0:1;

consider i being Element of NAT such that

A5: [x,y] = [i,(i + 1)] and

i + 1 < n by A2;

( x = i & y = i + 1 ) by A5, XTUPLE_0:1;

hence contradiction by A4; :: thesis: verum