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)

proof

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;

hence the InternalRel of (n -SuccRelStr) is asymmetric ; :: according to NECKLACE:def 4 :: thesis: verum