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 set ; :: 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, Def7;
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 Def7;
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, ZFMISC_1:33;
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, ZFMISC_1:33;
hence contradiction by A4; :: thesis: verum

end;

hence the InternalRel of (n -SuccRelStr ) is asymmetric by RELAT_2:def 13; :: according to NECKLACE:def 5 :: thesis: verum